Bob is green. Charlie is blue. Gary is green. Green, rough things are white. If Gary is green then Gary is rough. If Gary is cold and Gary is young then Gary is blue. If something is green and cold then it is young. If Gary is round and Gary is young then Gary is blue. If something is white and round then it is blue. If Gary is white and Gary is blue then Gary is young. Blue things are round.
Bob is green.
("Bob" "is" "green" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Green, rough things are white.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If Gary is green then Gary is rough.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "rough" "+"))
If Gary is cold and Gary is young then Gary is blue.
((("Gary" "is" "cold" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "blue" "+"))
If something is green and cold then it is young.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If Gary is round and Gary is young then Gary is blue.
((("Gary" "is" "round" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "blue" "+"))
If something is white and round then it is blue.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If Gary is white and Gary is blue then Gary is young.
((("Gary" "is" "white" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "young" "+"))
Blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
Gary is green.
True
1
proof
[(triple3)]
("Gary" "is" "green" "+")
triple3
Gary is not green.
False
1
inv-proof
[(triple3)]
("Gary" "is" "green" "-")
triple3
Charlie is round.
True
2
proof
[(((triple2) -> rule8))]
("Charlie" "is" "round" "+")
((triple2) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple2) -> rule8))]
("Charlie" "is" "round" "-")
((triple2) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is round.
Unknown
rconc
[@2: Bob is round.[CWA. Example of deepest failure = (rule8 <- rule6 <- FAIL)]]
("Bob" "is" "round" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Bob is green.[(triple1)] Charlie is blue.[(triple2)] Gary is green.[(triple3)] @1: Charlie is round.[(((triple2) -> rule8))] Gary is rough.[(((triple3) -> rule2))] @2: Gary is white.[(((triple3 ((triple3) -> rule2)) -> rule1))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
((triple2) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple3) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2