Bob is cold. Bob is quiet. Bob is smart. Charlie is green. Charlie is rough. Charlie is smart. Harry is green. Harry is quiet. Harry is rough. Harry is white. If Charlie is smart and Charlie is white then Charlie is big. All big, smart things are white.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
If Charlie is smart and Charlie is white then Charlie is big.
((("Charlie" "is" "smart" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "big" "+"))
All big, smart things are white.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
Charlie is smart.
True
1
proof
[(triple6)]
("Charlie" "is" "smart" "+")
triple6
Charlie is not smart.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "smart" "-")
triple6
Charlie is not white.
Unknown
inv-rconc
[@2: Charlie is white.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Charlie" "is" "white" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is cold.[(triple1)] Bob is quiet.[(triple2)] Bob is smart.[(triple3)] Charlie is green.[(triple4)] Charlie is rough.[(triple5)] Charlie is smart.[(triple6)] Harry is green.[(triple7)] Harry is quiet.[(triple8)] Harry is rough.[(triple9)] Harry is white.[(triple10)]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
Harry is quiet.
("Harry" "is" "quiet" "+")
triple8
Harry is rough.
("Harry" "is" "rough" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10