Bob is rough. Charlie is furry. Gary is white. All red things are blue. All furry things are blue. If something is cold then it is red. If something is rough then it is cold. Furry, blue things are cold. If Bob is red and Bob is furry then Bob is white.
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Gary is white.
("Gary" "is" "white" "+")
All red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
All furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
If something is cold then it is red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If something is rough then it is cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Furry, blue things are cold.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If Bob is red and Bob is furry then Bob is white.
((("Bob" "is" "red" "+") ("Bob" "is" "furry" "+")) -> ("Bob" "is" "white" "+"))
Gary is white.
True
1
proof
[(triple3)]
("Gary" "is" "white" "+")
triple3
Gary is not white.
False
1
inv-proof
[(triple3)]
("Gary" "is" "white" "-")
triple3
Charlie is blue.
True
2
proof
[(((triple2) -> rule2))]
("Charlie" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "cold" "-")
((triple1) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("Bob" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Charlie is not cold.
False
4
inv-proof
[(((triple2 ((triple2) -> rule2)) -> rule5))]
("Charlie" "is" "cold" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Gary is not blue.
Unknown
inv-rconc
[@3: Gary is blue.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule4 <- FAIL)]]
("Gary" "is" "blue" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "cold" "+")
Gary is not red.
Unknown
inv-rconc
[@2: Gary is red.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Gary" "is" "red" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Bob is rough.[(triple1)] Charlie is furry.[(triple2)] Gary is white.[(triple3)] @1: Bob is cold.[(((triple1) -> rule4))] Charlie is blue.[(((triple2) -> rule2))] @2: Bob is red.[(((((triple1) -> rule4)) -> rule3))] Charlie is cold.[(((triple2 ((triple2) -> rule2)) -> rule5))] @3: Bob is blue.[(((((((triple1) -> rule4)) -> rule3)) -> rule1))] Charlie is red.[(((((triple2 ((triple2) -> rule2)) -> rule5)) -> rule3))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3