Anne is young. Bob is red. Gary is big. If Anne is not round and Anne is not young then Anne is rough. If something is big and quiet then it is rough. If something is young and not red then it is rough. If something is round and young then it is big. All big things are quiet. If Gary is big and Gary is rough then Gary is blue.
Anne is young.
("Anne" "is" "young" "+")
Bob is red.
("Bob" "is" "red" "+")
Gary is big.
("Gary" "is" "big" "+")
If Anne is not round and Anne is not young then Anne is rough.
((("Anne" "is" "round" "~") ("Anne" "is" "young" "~")) -> ("Anne" "is" "rough" "+"))
If something is big and quiet then it is rough.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is young and not red then it is rough.
((("something" "is" "young" "+") ("something" "is" "red" "~")) -> ("something" "is" "rough" "+"))
If something is round and young then it is big.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
All big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If Gary is big and Gary is rough then Gary is blue.
((("Gary" "is" "big" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "blue" "+"))
Gary is big.
True
1
proof
[(triple3)]
("Gary" "is" "big" "+")
triple3
Anne is not young.
False
1
inv-proof
[(triple1)]
("Anne" "is" "young" "-")
triple1
Gary is quiet.
True
2
proof
[(((triple3) -> rule5))]
("Gary" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple3) -> rule5))]
("Gary" "is" "quiet" "-")
((triple3) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
True
4
proof
[(((triple3 ((triple3) -> rule5)) -> rule2))]
("Gary" "is" "rough" "+")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not rough.
False
4
inv-proof
[(((triple3 ((triple3) -> rule5)) -> rule2))]
("Gary" "is" "rough" "-")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is blue.
True
6
proof
[(((triple3 ((triple3 ((triple3) -> rule5)) -> rule2)) -> rule6))]
("Gary" "is" "blue" "+")
((triple3 ((triple3 ((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is not blue.
False
6
inv-proof
[(((triple3 ((triple3 ((triple3) -> rule5)) -> rule2)) -> rule6))]
("Gary" "is" "blue" "-")
((triple3 ((triple3 ((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Bob is not rough.
Unknown
inv-rconc
[@2: Bob is rough.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Bob" "is" "rough" "-")
Anne is big.
Unknown
rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "big" "+")
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "big" "-")
Anne is rough.
Unknown
rconc
[@2: Anne is rough.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Anne" "is" "rough" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is young.[(triple1)] Bob is red.[(triple2)] Gary is big.[(triple3)] @1: Gary is quiet.[(((triple3) -> rule5))] @2: Gary is rough.[(((triple3 ((triple3) -> rule5)) -> rule2))] @3: Gary is blue.[(((triple3 ((triple3 ((triple3) -> rule5)) -> rule2)) -> rule6))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((triple3 ((triple3 ((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3