Charlie is rough. Dave is kind. Gary is cold. All red things are cold. Big, kind things are cold. If Gary is blue then Gary is red. Cold things are big. All big, green things are blue. All blue things are cold. If something is cold then it is red. Big things are rough.
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Gary is cold.
("Gary" "is" "cold" "+")
All red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
Big, kind things are cold.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If Gary is blue then Gary is red.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "red" "+"))
Cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
All big, green things are blue.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
All blue things are cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If something is cold then it is red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Gary is cold.
True
1
proof
[(triple3)]
("Gary" "is" "cold" "+")
triple3
Gary is not cold.
False
1
inv-proof
[(triple3)]
("Gary" "is" "cold" "-")
triple3
Gary is big.
True
2
proof
[(((triple3) -> rule4))]
("Gary" "is" "big" "+")
((triple3) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not red.
False
2
inv-proof
[(((triple3) -> rule7))]
("Gary" "is" "red" "-")
((triple3) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
True
3
proof
[(((((triple3) -> rule4)) -> rule8))]
("Gary" "is" "rough" "+")
((((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not rough.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule8))]
("Gary" "is" "rough" "-")
((((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Dave is not rough.
Unknown
inv-rconc
[@6: Dave is rough.[CWA. Example of deepest failure = (rule8 <- rule4 <- rule1 <- rule7 <- rule6 <- rule5 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is big.
Unknown
rconc
[@5: Dave is big.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule7 <- rule6 <- rule5 <- FAIL)]]
("Dave" "is" "big" "+")
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "blue" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Charlie is rough.[(triple1)] Dave is kind.[(triple2)] Gary is cold.[(triple3)] @1: Gary is big.[(((triple3) -> rule4))] Gary is red.[(((triple3) -> rule7))] @2: Gary is rough.[(((((triple3) -> rule4)) -> rule8))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
((triple3) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple3) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2