Bob is red. Charlie is blue. All cold things are red. Red, big things are rough. If Charlie is blue then Charlie is cold. All rough things are blue. If something is rough then it is red. Young, big things are rough. If Bob is big then Bob is cold. All young, cold things are big.
Bob is red.
("Bob" "is" "red" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
All cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Red, big things are rough.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If Charlie is blue then Charlie is cold.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "cold" "+"))
All rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If something is rough then it is red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
Young, big things are rough.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If Bob is big then Bob is cold.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "cold" "+"))
All young, cold things are big.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Charlie is blue.
True
1
proof
[(triple2)]
("Charlie" "is" "blue" "+")
triple2
Bob is not red.
False
1
inv-proof
[(triple1)]
("Bob" "is" "red" "-")
triple1
Charlie is cold.
True
2
proof
[(((triple2) -> rule3))]
("Charlie" "is" "cold" "+")
((triple2) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple2) -> rule3))]
("Charlie" "is" "cold" "-")
((triple2) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("Charlie" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not red.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("Charlie" "is" "red" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "big" "-")
Charlie is rough.
Unknown
rconc
[@2: Charlie is rough.[CWA. Example of deepest failure = (rule2 <- rule8 <- FAIL)]]
("Charlie" "is" "rough" "+")
Bob is not rough.
Unknown
inv-rconc
[@2: Bob is rough.[CWA. Example of deepest failure = (rule2 <- rule8 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Bob is red.[(triple1)] Charlie is blue.[(triple2)] @1: Charlie is cold.[(((triple2) -> rule3))] @2: Charlie is red.[(((((triple2) -> rule3)) -> rule1))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple2) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2