Anne is big. Anne is blue. Anne is cold. Anne is rough. Anne is white. Harry is big. Harry is blue. Harry is kind. Harry is quiet. Harry is rough. If someone is cold then they are quiet. Blue, quiet people are kind.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is cold then they are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
Blue, quiet people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Harry is kind.
True
1
proof
[(triple8 OR ((triple7 triple9) -> rule2))]
("Harry" "is" "kind" "+")
triple8
((triple7 triple9) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not quiet.
False
1
inv-proof
[(triple9)]
("Harry" "is" "quiet" "-")
triple9
Anne is quiet.
True
2
proof
[(((triple3) -> rule1))]
("Anne" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple3) -> rule1))]
("Anne" "is" "quiet" "-")
((triple3) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is kind.
True
4
proof
[(((triple2 ((triple3) -> rule1)) -> rule2))]
("Anne" "is" "kind" "+")
((triple2 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not kind.
False
4
inv-proof
[(((triple2 ((triple3) -> rule1)) -> rule2))]
("Anne" "is" "kind" "-")
((triple2 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is cold.[(triple3)] Anne is rough.[(triple4)] Anne is white.[(triple5)] Harry is big.[(triple6)] Harry is blue.[(triple7)] Harry is kind.[(triple8 OR ((triple7 triple9) -> rule2))] Harry is quiet.[(triple9)] Harry is rough.[(triple10)] @1: Anne is quiet.[(((triple3) -> rule1))] @2: Anne is kind.[(((triple2 ((triple3) -> rule1)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is cold.
("Anne" "is" "cold" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is blue.
("Harry" "is" "blue" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
triple8
((triple7 triple9) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple2 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2