Anne is big. Charlie is kind. Gary is quiet. Harry is quiet. Kind people are big. If Anne is kind and Anne is white then Anne is cold. If someone is big and round then they are quiet. If Harry is round then Harry is white. If someone is kind then they are rough. All round, kind people are cold.
Anne is big.
("Anne" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If Anne is kind and Anne is white then Anne is cold.
((("Anne" "is" "kind" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "cold" "+"))
If someone is big and round then they are quiet.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If Harry is round then Harry is white.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "white" "+"))
If someone is kind then they are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
All round, kind people are cold.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Charlie is kind.
True
1
proof
[(triple2)]
("Charlie" "is" "kind" "+")
triple2
Harry is not quiet.
False
1
inv-proof
[(triple4)]
("Harry" "is" "quiet" "-")
triple4
Charlie is big.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "big" "+")
((triple2) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple2) -> rule5))]
("Charlie" "is" "rough" "-")
((triple2) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "quiet" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "cold" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is big.[(triple1)] Charlie is kind.[(triple2)] Gary is quiet.[(triple3)] Harry is quiet.[(triple4)] @1: Charlie is big.[(((triple2) -> rule1))] Charlie is rough.[(((triple2) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
((triple2) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1