Anne is blue. Anne is cold. Anne is furry. Anne is kind. Charlie is cold. Charlie is kind. Charlie is quiet. Erin is furry. Erin is quiet. Erin is young. Harry is blue. Harry is cold. Harry is furry. Harry is quiet. Harry is red. If something is young and blue then it is kind. All young things are blue. If Anne is cold and Anne is young then Anne is kind. Cold, red things are quiet. All kind things are red. Cold things are young.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
If something is young and blue then it is kind.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
All young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If Anne is cold and Anne is young then Anne is kind.
((("Anne" "is" "cold" "+") ("Anne" "is" "young" "+")) -> ("Anne" "is" "kind" "+"))
Cold, red things are quiet.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
All kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
Cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
Harry is cold.
True
1
proof
[(triple12)]
("Harry" "is" "cold" "+")
triple12
Erin is not young.
False
1
inv-proof
[(triple10)]
("Erin" "is" "young" "-")
triple10
Erin is blue.
True
2
proof
[(((triple10) -> rule2))]
("Erin" "is" "blue" "+")
((triple10) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple2) -> rule6))]
("Anne" "is" "young" "-")
((triple2) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is kind.
True
4
proof
[(((triple10 ((triple10) -> rule2)) -> rule1))]
("Erin" "is" "kind" "+")
((triple10 ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Harry is not kind.
False
4
inv-proof
[(((((triple12) -> rule6) triple11) -> rule1) OR ((((triple12) -> rule6) ((((triple12) -> rule6)) -> rule2)) -> rule1))]
("Harry" "is" "kind" "-")
((((triple12) -> (rule6 % int2)) triple11) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple12) -> (rule6 % int3)) ((((triple12) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Erin is red.
True
5
proof
[(((((triple10 ((triple10) -> rule2)) -> rule1)) -> rule5))]
("Erin" "is" "red" "+")
((((triple10 ((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is not red.
False
5
inv-proof
[(((((triple10 ((triple10) -> rule2)) -> rule1)) -> rule5))]
("Erin" "is" "red" "-")
((((triple10 ((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Anne is blue.[(triple1 OR ((((triple2) -> rule6)) -> rule2))] Anne is cold.[(triple2)] Anne is furry.[(triple3)] Anne is kind.[(triple4 OR ((triple2 ((triple2) -> rule6)) -> rule3) OR ((((triple2) -> rule6) triple1) -> rule1) OR ((((triple2) -> rule6) ((((triple2) -> rule6)) -> rule2)) -> rule1))] Charlie is cold.[(triple5)] Charlie is kind.[(triple6 OR ((((triple5) -> rule6) ((((triple5) -> rule6)) -> rule2)) -> rule1))] Charlie is quiet.[(triple7 OR ((triple5 ((triple6) -> rule5)) -> rule4) OR ((triple5 ((((((triple5) -> rule6) ((((triple5) -> rule6)) -> rule2)) -> rule1)) -> rule5)) -> rule4))] Erin is furry.[(triple8)] Erin is quiet.[(triple9)] Erin is young.[(triple10)] Harry is blue.[(triple11 OR ((((triple12) -> rule6)) -> rule2))] Harry is cold.[(triple12)] Harry is furry.[(triple13)] Harry is quiet.[(triple14 OR ((triple12 triple15) -> rule4) OR ((triple12 ((((((triple12) -> rule6) triple11) -> rule1)) -> rule5)) -> rule4) OR ((triple12 ((((((triple12) -> rule6) ((((triple12) -> rule6)) -> rule2)) -> rule1)) -> rule5)) -> rule4))] Harry is red.[(triple15 OR ((((((triple12) -> rule6) triple11) -> rule1)) -> rule5) OR ((((((triple12) -> rule6) ((((triple12) -> rule6)) -> rule2)) -> rule1)) -> rule5))] @1: Anne is red.[(((triple4) -> rule5) OR ((((triple2 ((triple2) -> rule6)) -> rule3)) -> rule5) OR ((((((triple2) -> rule6) triple1) -> rule1)) -> rule5) OR ((((((triple2) -> rule6) ((((triple2) -> rule6)) -> rule2)) -> rule1)) -> rule5))] Anne is young.[(((triple2) -> rule6))] Charlie is red.[(((triple6) -> rule5) OR ((((((triple5) -> rule6) ((((triple5) -> rule6)) -> rule2)) -> rule1)) -> rule5))] Charlie is young.[(((triple5) -> rule6))] Erin is blue.[(((triple10) -> rule2))] Harry is young.[(((triple12) -> rule6))] @2: Anne is quiet.[(((triple2 ((triple4) -> rule5)) -> rule4) OR ((triple2 ((((triple2 ((triple2) -> rule6)) -> rule3)) -> rule5)) -> rule4) OR ((triple2 ((((((triple2) -> rule6) triple1) -> rule1)) -> rule5)) -> rule4) OR ((triple2 ((((((triple2) -> rule6) ((((triple2) -> rule6)) -> rule2)) -> rule1)) -> rule5)) -> rule4))] Charlie is blue.[(((((triple5) -> rule6)) -> rule2))] Erin is kind.[(((triple10 ((triple10) -> rule2)) -> rule1))] Harry is kind.[(((((triple12) -> rule6) triple11) -> rule1) OR ((((triple12) -> rule6) ((((triple12) -> rule6)) -> rule2)) -> rule1))] @3: Erin is red.[(((((triple10 ((triple10) -> rule2)) -> rule1)) -> rule5))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
triple4
((triple2 ((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((triple2) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((triple2) -> (rule6 % int3)) ((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
Charlie is kind.
("Charlie" "is" "kind" "+")
triple6
((((triple5) -> (rule6 % int3)) ((((triple5) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple7
((triple5 ((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((triple5 ((((((triple5) -> (rule6 % int5)) ((((triple5) -> (rule6 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is young.
("Charlie" "is" "young" "+")
int5
Erin is furry.
("Erin" "is" "furry" "+")
triple8
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
Erin is young.
("Erin" "is" "young" "+")
triple10
Harry is blue.
("Harry" "is" "blue" "+")
triple11
((((triple12) -> (rule6 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple12
Harry is furry.
("Harry" "is" "furry" "+")
triple13
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
((triple12 triple15) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple12 ((((((triple12) -> (rule6 % int4)) triple11) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
((triple12 ((((((triple12) -> (rule6 % int5)) ((((triple12) -> (rule6 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is young.
("Harry" "is" "young" "+")
int5
Harry is red.
("Harry" "is" "red" "+")
triple15
((((((triple12) -> (rule6 % int3)) triple11) -> (rule1 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((((triple12) -> (rule6 % int4)) ((((triple12) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
((triple4) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((((triple2) -> (rule6 % int3)) triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((((triple2) -> (rule6 % int4)) ((((triple2) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
((triple2) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple6) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((((triple5) -> (rule6 % int4)) ((((triple5) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is young.
("Charlie" "is" "young" "+")
((triple5) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple10) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple12) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple2 ((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((triple2 ((((triple2 ((triple2) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
((triple2 ((((((triple2) -> (rule6 % int4)) triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
((triple2 ((((((triple2) -> (rule6 % int5)) ((((triple2) -> (rule6 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
int5
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple5) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((triple10 ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple12) -> (rule6 % int2)) triple11) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple12) -> (rule6 % int3)) ((((triple12) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
((((triple10 ((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3