Anne is green. Anne is quiet. Bob is blue. Bob is green. Charlie is cold. Gary is big. Gary is blue. Blue things are quiet. Big things are quiet. Quiet, big things are rough. Cold things are rough. If something is cold then it is blue. If something is rough and quiet then it is cold.
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
Big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Quiet, big things are rough.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If something is cold then it is blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something is rough and quiet then it is cold.
((("something" "is" "rough" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
Bob is blue.
True
1
proof
[(triple3)]
("Bob" "is" "blue" "+")
triple3
Anne is not quiet.
False
1
inv-proof
[(triple2)]
("Anne" "is" "quiet" "-")
triple2
Bob is quiet.
True
2
proof
[(((triple3) -> rule1))]
("Bob" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple3) -> rule1))]
("Bob" "is" "quiet" "-")
((triple3) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Charlie is quiet.
True
3
proof
[(((((triple5) -> rule5)) -> rule1))]
("Charlie" "is" "quiet" "+")
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not quiet.
False
3
inv-proof
[(((((triple5) -> rule5)) -> rule1))]
("Charlie" "is" "quiet" "-")
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Gary is cold.
True
7
proof
[(((((((triple6) -> rule2) triple6) -> rule3) ((triple6) -> rule2)) -> rule6) OR ((((((triple6) -> rule2) triple6) -> rule3) ((triple7) -> rule1)) -> rule6) OR ((((((triple7) -> rule1) triple6) -> rule3) ((triple6) -> rule2)) -> rule6) OR ((((((triple7) -> rule1) triple6) -> rule3) ((triple7) -> rule1)) -> rule6))]
("Gary" "is" "cold" "+")
((((((triple6) -> (rule2 % int3)) triple6) -> (rule3 % int2)) ((triple6) -> (rule2 % int3))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple6) -> (rule2 % int3)) triple6) -> (rule3 % int2)) ((triple7) -> (rule1 % int3))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple7) -> (rule1 % int3)) triple6) -> (rule3 % int2)) ((triple6) -> (rule2 % int3))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple7) -> (rule1 % int3)) triple6) -> (rule3 % int2)) ((triple7) -> (rule1 % int3))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is not cold.
False
7
inv-proof
[(((((((triple6) -> rule2) triple6) -> rule3) ((triple6) -> rule2)) -> rule6) OR ((((((triple6) -> rule2) triple6) -> rule3) ((triple7) -> rule1)) -> rule6) OR ((((((triple7) -> rule1) triple6) -> rule3) ((triple6) -> rule2)) -> rule6) OR ((((((triple7) -> rule1) triple6) -> rule3) ((triple7) -> rule1)) -> rule6))]
("Gary" "is" "cold" "-")
((((((triple6) -> (rule2 % int3)) triple6) -> (rule3 % int2)) ((triple6) -> (rule2 % int3))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple6) -> (rule2 % int3)) triple6) -> (rule3 % int2)) ((triple7) -> (rule1 % int3))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple7) -> (rule1 % int3)) triple6) -> (rule3 % int2)) ((triple6) -> (rule2 % int3))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple7) -> (rule1 % int3)) triple6) -> (rule3 % int2)) ((triple7) -> (rule1 % int3))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Anne is not cold.
Unknown
inv-rconc
[@2: Anne is cold.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is rough.
Unknown
rconc
[@3: Anne is rough.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule3 <- FAIL)]]
("Anne" "is" "rough" "+")
Bob is not cold.
Unknown
inv-rconc
[@2: Bob is cold.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Bob" "is" "cold" "-")
Anne is blue.
Unknown
rconc
[@3: Anne is blue.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule3 <- FAIL)]]
("Anne" "is" "blue" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Anne is green.[(triple1)] Anne is quiet.[(triple2)] Bob is blue.[(triple3)] Bob is green.[(triple4)] Charlie is cold.[(triple5)] Gary is big.[(triple6)] Gary is blue.[(triple7 OR ((((((((triple6) -> rule2) triple6) -> rule3) ((triple6) -> rule2)) -> rule6)) -> rule5))] @1: Bob is quiet.[(((triple3) -> rule1))] Charlie is blue.[(((triple5) -> rule5))] Charlie is rough.[(((triple5) -> rule4))] Gary is quiet.[(((triple6) -> rule2) OR ((triple7) -> rule1))] @2: Charlie is quiet.[(((((triple5) -> rule5)) -> rule1))] Gary is rough.[(((((triple6) -> rule2) triple6) -> rule3) OR ((((triple7) -> rule1) triple6) -> rule3))] @3: Gary is cold.[(((((((triple6) -> rule2) triple6) -> rule3) ((triple6) -> rule2)) -> rule6) OR ((((((triple6) -> rule2) triple6) -> rule3) ((triple7) -> rule1)) -> rule6) OR ((((((triple7) -> rule1) triple6) -> rule3) ((triple6) -> rule2)) -> rule6) OR ((((((triple7) -> rule1) triple6) -> rule3) ((triple7) -> rule1)) -> rule6))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple7
((((((((triple6) -> (rule2 % int4)) triple6) -> (rule3 % int3)) ((triple6) -> (rule2 % int4))) -> (rule6 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple5) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple5) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple6) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple7) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((((triple6) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple7) -> (rule1 % int2)) triple6) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple6) -> (rule2 % int3)) triple6) -> (rule3 % int2)) ((triple6) -> (rule2 % int3))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple6) -> (rule2 % int3)) triple6) -> (rule3 % int2)) ((triple7) -> (rule1 % int3))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple7) -> (rule1 % int3)) triple6) -> (rule3 % int2)) ((triple6) -> (rule2 % int3))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple7) -> (rule1 % int3)) triple6) -> (rule3 % int2)) ((triple7) -> (rule1 % int3))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3