Anne is smart. Charlie is not smart. Harry is quiet. Round people are big. If Charlie is not cold then Charlie is green. All quiet people are green.
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If Charlie is not cold then Charlie is green.
((("Charlie" "is" "cold" "~")) -> ("Charlie" "is" "green" "+"))
All quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Charlie is not smart.
True
1
proof
[(triple2)]
("Charlie" "is" "smart" "-")
triple2
Charlie is smart.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "smart" "+")
triple2
Harry is green.
True
2
proof
[(((triple3) -> rule3))]
("Harry" "is" "green" "+")
((triple3) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple3) -> rule3))]
("Harry" "is" "green" "-")
((triple3) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "-")
Anne is green.
Unknown
rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "green" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is smart.[(triple1)] Charlie is not smart.[(triple2)] Harry is quiet.[(triple3)] @1: Harry is green.[(((triple3) -> rule3))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
((triple3) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1