Charlie is red. Dave is cold. Dave is red. All red, big things are white. Green, big things are red. If something is red then it is smart. All red things are cold. If something is white then it is red. All young, smart things are big. All green things are white. If something is white and young then it is big.
Charlie is red.
("Charlie" "is" "red" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
All red, big things are white.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
Green, big things are red.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is red then it is smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
All red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something is white then it is red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
All young, smart things are big.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
All green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is white and young then it is big.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Dave is cold.
True
1
proof
[(triple2 OR ((triple3) -> rule4))]
("Dave" "is" "cold" "+")
triple2
((triple3) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule4))]
("Dave" "is" "cold" "-")
triple2
((triple3) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
True
2
proof
[(((triple3) -> rule3))]
("Dave" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple3) -> rule3))]
("Dave" "is" "smart" "-")
((triple3) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "big" "-")
Charlie is white.
Unknown
rconc
[@2: Charlie is white.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Charlie is red.[(triple1)] Dave is cold.[(triple2 OR ((triple3) -> rule4))] Dave is red.[(triple3)] @1: Charlie is cold.[(((triple1) -> rule4))] Charlie is smart.[(((triple1) -> rule3))] Dave is smart.[(((triple3) -> rule3))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
((triple3) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1