Anne is blue. Anne is green. Anne is nice. Anne is quiet. Anne is round. Charlie is blue. Charlie is cold. Charlie is nice. Charlie is rough. Harry is blue. Harry is cold. Harry is green. Harry is nice. Harry is quiet. Harry is rough. Harry is round. All nice, cold people are round. Blue people are green. All blue people are cold.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
All nice, cold people are round.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
Blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
All blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
Harry is blue.
True
1
proof
[(triple10)]
("Harry" "is" "blue" "+")
triple10
Charlie is not rough.
False
1
inv-proof
[(triple9)]
("Charlie" "is" "rough" "-")
triple9
Anne is cold.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Charlie is not round.
False
3
inv-proof
[(((triple8 triple7) -> rule1) OR ((triple8 ((triple6) -> rule3)) -> rule1))]
("Charlie" "is" "round" "-")
((triple8 triple7) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple8 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Anne is blue.[(triple1)] Anne is green.[(triple2 OR ((triple1) -> rule2))] Anne is nice.[(triple3)] Anne is quiet.[(triple4)] Anne is round.[(triple5 OR ((triple3 ((triple1) -> rule3)) -> rule1))] Charlie is blue.[(triple6)] Charlie is cold.[(triple7 OR ((triple6) -> rule3))] Charlie is nice.[(triple8)] Charlie is rough.[(triple9)] Harry is blue.[(triple10)] Harry is cold.[(triple11 OR ((triple10) -> rule3))] Harry is green.[(triple12 OR ((triple10) -> rule2))] Harry is nice.[(triple13)] Harry is quiet.[(triple14)] Harry is rough.[(triple15)] Harry is round.[(triple16 OR ((triple13 triple11) -> rule1) OR ((triple13 ((triple10) -> rule3)) -> rule1))] @1: Anne is cold.[(((triple1) -> rule3))] Charlie is green.[(((triple6) -> rule2))] Charlie is round.[(((triple8 triple7) -> rule1) OR ((triple8 ((triple6) -> rule3)) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
((triple3 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
Charlie is cold.
("Charlie" "is" "cold" "+")
triple7
((triple6) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple8
Charlie is rough.
("Charlie" "is" "rough" "+")
triple9
Harry is blue.
("Harry" "is" "blue" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
triple11
((triple10) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple12
((triple10) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple13
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Harry is round.
("Harry" "is" "round" "+")
triple16
((triple13 triple11) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple13 ((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple6) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple8 triple7) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple8 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2