Anne is rough. Anne is young. Bob is not white. Bob is young. Gary is cold. Harry is cold. Harry is rough. If something is rough then it is quiet. Rough, smart things are not cold. Young things are cold. If Bob is white then Bob is rough. Cold things are rough. If Bob is not quiet then Bob is red.
Anne is rough.
("Anne" "is" "rough" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is not white.
("Bob" "is" "white" "-")
Bob is young.
("Bob" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If something is rough then it is quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Rough, smart things are not cold.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "-"))
Young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If Bob is white then Bob is rough.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "rough" "+"))
Cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If Bob is not quiet then Bob is red.
((("Bob" "is" "quiet" "~")) -> ("Bob" "is" "red" "+"))
Bob is young.
True
1
proof
[(triple4)]
("Bob" "is" "young" "+")
triple4
Anne is not young.
False
1
inv-proof
[(triple2)]
("Anne" "is" "young" "-")
triple2
Bob is cold.
True
2
proof
[(((triple4) -> rule3))]
("Bob" "is" "cold" "+")
((triple4) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple4) -> rule3))]
("Bob" "is" "cold" "-")
((triple4) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
True
3
proof
[(((((triple4) -> rule3)) -> rule5))]
("Bob" "is" "rough" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not rough.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule5))]
("Bob" "is" "rough" "-")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is quiet.
True
4
proof
[(((((((triple4) -> rule3)) -> rule5)) -> rule1))]
("Bob" "is" "quiet" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not quiet.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule5)) -> rule1))]
("Bob" "is" "quiet" "-")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "red" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Anne is rough.[(triple1 OR ((((triple2) -> rule3)) -> rule5))] Anne is young.[(triple2)] Bob is not white.[(triple3)] Bob is young.[(triple4)] Gary is cold.[(triple5)] Harry is cold.[(triple6)] Harry is rough.[(triple7 OR ((triple6) -> rule5))] @1: Anne is cold.[(((triple2) -> rule3))] Anne is quiet.[(((triple1) -> rule1) OR ((((((triple2) -> rule3)) -> rule5)) -> rule1))] Bob is cold.[(((triple4) -> rule3))] Gary is rough.[(((triple5) -> rule5))] Harry is quiet.[(((triple7) -> rule1) OR ((((triple6) -> rule5)) -> rule1))] @2: Bob is rough.[(((((triple4) -> rule3)) -> rule5))] Gary is quiet.[(((((triple5) -> rule5)) -> rule1))] @3: Bob is quiet.[(((((((triple4) -> rule3)) -> rule5)) -> rule1))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple2
Bob is not white.
("Bob" "is" "white" "-")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
((triple6) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((triple2) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
((triple4) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple5) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple7) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3