Bob is blue. Bob is rough. Bob is white. Gary is cold. Gary is green. Gary is nice. Gary is round. Blue things are white. If something is blue then it is green. Rough, round things are nice. Round, blue things are rough. All nice things are cold. If something is nice and round then it is blue.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
Blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
If something is blue then it is green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Rough, round things are nice.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Round, blue things are rough.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
All nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is nice and round then it is blue.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Bob is white.
True
1
proof
[(triple3 OR ((triple1) -> rule1))]
("Bob" "is" "white" "+")
triple3
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Gary is not nice.
False
1
inv-proof
[(triple6)]
("Gary" "is" "nice" "-")
triple6
Gary is blue.
True
3
proof
[(((triple6 triple7) -> rule6))]
("Gary" "is" "blue" "+")
((triple6 triple7) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
3
inv-proof
[(((triple6 triple7) -> rule6))]
("Gary" "is" "blue" "-")
((triple6 triple7) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is rough.
True
5
proof
[(((triple7 ((triple6 triple7) -> rule6)) -> rule4))]
("Gary" "is" "rough" "+")
((triple7 ((triple6 triple7) -> (rule6 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not rough.
False
5
inv-proof
[(((triple7 ((triple6 triple7) -> rule6)) -> rule4))]
("Gary" "is" "rough" "-")
((triple7 ((triple6 triple7) -> (rule6 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Bob is not cold.
Unknown
inv-rconc
[@2: Bob is cold.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is blue.[(triple1)] Bob is rough.[(triple2)] Bob is white.[(triple3 OR ((triple1) -> rule1))] Gary is cold.[(triple4 OR ((triple6) -> rule5))] Gary is green.[(triple5 OR ((((triple6 triple7) -> rule6)) -> rule2))] Gary is nice.[(triple6)] Gary is round.[(triple7)] @1: Bob is green.[(((triple1) -> rule2))] Gary is blue.[(((triple6 triple7) -> rule6))] @2: Gary is rough.[(((triple7 ((triple6 triple7) -> rule6)) -> rule4))] Gary is white.[(((((triple6 triple7) -> rule6)) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple4
((triple6) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple5
((((triple6 triple7) -> (rule6 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple6 triple7) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple7 ((triple6 triple7) -> (rule6 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((triple6 triple7) -> (rule6 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2