Dave is green. Dave is smart. Harry is red. All smart, big things are cold. Smart things are big. If Dave is big and Dave is smart then Dave is round. If Harry is blue then Harry is cold. Big things are green. If something is big and red then it is blue.
Dave is green.
("Dave" "is" "green" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is red.
("Harry" "is" "red" "+")
All smart, big things are cold.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
Smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If Dave is big and Dave is smart then Dave is round.
((("Dave" "is" "big" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "round" "+"))
If Harry is blue then Harry is cold.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "cold" "+"))
Big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If something is big and red then it is blue.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Dave is smart.
True
1
proof
[(triple2)]
("Dave" "is" "smart" "+")
triple2
Harry is not red.
False
1
inv-proof
[(triple3)]
("Harry" "is" "red" "-")
triple3
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "big" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Dave is green.[(triple1 OR ((((triple2) -> rule2)) -> rule5))] Dave is smart.[(triple2)] Harry is red.[(triple3)] @1: Dave is big.[(((triple2) -> rule2))] @2: Dave is cold.[(((triple2 ((triple2) -> rule2)) -> rule1))] Dave is round.[(((((triple2) -> rule2) triple2) -> rule3))]
Dave is green.
("Dave" "is" "green" "+")
triple1
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Harry is red.
("Harry" "is" "red" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
((triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2