Anne is quiet. Anne is white. Bob is smart. All young people are cold. If someone is smart then they are rough. Blue, white people are young. If someone is white and rough then they are blue. If someone is smart and white then they are quiet. Smart people are cold. All quiet, cold people are young. If someone is quiet then they are rough.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is smart.
("Bob" "is" "smart" "+")
All young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If someone is smart then they are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Blue, white people are young.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
If someone is white and rough then they are blue.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If someone is smart and white then they are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
Smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
All quiet, cold people are young.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If someone is quiet then they are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Bob is cold.
True
2
proof
[(((triple3) -> rule6))]
("Bob" "is" "cold" "+")
((triple3) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Anne is not rough.
False
2
inv-proof
[(((triple1) -> rule8))]
("Anne" "is" "rough" "-")
((triple1) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is blue.
True
4
proof
[(((triple2 ((triple1) -> rule8)) -> rule4))]
("Anne" "is" "blue" "+")
((triple2 ((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not blue.
False
4
inv-proof
[(((triple2 ((triple1) -> rule8)) -> rule4))]
("Anne" "is" "blue" "-")
((triple2 ((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is young.
True
6
proof
[(((((triple2 ((triple1) -> rule8)) -> rule4) triple2) -> rule3))]
("Anne" "is" "young" "+")
((((triple2 ((triple1) -> (rule8 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not young.
False
6
inv-proof
[(((((triple2 ((triple1) -> rule8)) -> rule4) triple2) -> rule3))]
("Anne" "is" "young" "-")
((((triple2 ((triple1) -> (rule8 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is blue.
Unknown
rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "blue" "+")
Bob is not young.
Unknown
inv-rconc
[@2: Bob is young.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("Bob" "is" "young" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is quiet.[(triple1)] Anne is white.[(triple2)] Bob is smart.[(triple3)] @1: Anne is rough.[(((triple1) -> rule8))] Bob is cold.[(((triple3) -> rule6))] Bob is rough.[(((triple3) -> rule2))] @2: Anne is blue.[(((triple2 ((triple1) -> rule8)) -> rule4))] @3: Anne is young.[(((((triple2 ((triple1) -> rule8)) -> rule4) triple2) -> rule3))] @4: Anne is cold.[(((((((triple2 ((triple1) -> rule8)) -> rule4) triple2) -> rule3)) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((triple3) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple3) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((triple2 ((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((triple2 ((triple1) -> (rule8 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
((((((triple2 ((triple1) -> (rule8 % int4))) -> (rule4 % int3)) triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4