Bob is cold. Bob is red. Bob is round. Charlie is red. Dave is blue. Dave is round. Gary is young. All blue, round people are cold. If someone is round and not red then they are cold. Young people are cold.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
All blue, round people are cold.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If someone is round and not red then they are cold.
((("someone" "is" "round" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "cold" "+"))
Young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
Bob is cold.
True
1
proof
[(triple1)]
("Bob" "is" "cold" "+")
triple1
Dave is not round.
False
1
inv-proof
[(triple6)]
("Dave" "is" "round" "-")
triple6
Gary is cold.
True
2
proof
[(((triple7) -> rule3))]
("Gary" "is" "cold" "+")
((triple7) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple7) -> rule3))]
("Gary" "is" "cold" "-")
((triple7) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Bob is cold.[(triple1)] Bob is red.[(triple2)] Bob is round.[(triple3)] Charlie is red.[(triple4)] Dave is blue.[(triple5)] Dave is round.[(triple6)] Gary is young.[(triple7)] @1: Dave is cold.[(((triple5 triple6) -> rule1))] Gary is cold.[(((triple7) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Dave is cold.
("Dave" "is" "cold" "+")
((triple5 triple6) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple7) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1