Anne is nice. Charlie is blue. Charlie is nice. Charlie is red. Gary is blue. Gary is white. Harry is cold. All young people are blue. If someone is young and not smart then they are not red. All blue people are red. If someone is white and young then they are red. If someone is red and blue then they are white. If someone is red then they are cold. If someone is nice then they are cold. If someone is smart and cold then they are young. If someone is cold then they are young.
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
All young people are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
If someone is young and not smart then they are not red.
((("someone" "is" "young" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "red" "-"))
All blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If someone is white and young then they are red.
((("someone" "is" "white" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If someone is red and blue then they are white.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice then they are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone is smart and cold then they are young.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If someone is cold then they are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
Gary is blue.
True
1
proof
[(triple5)]
("Gary" "is" "blue" "+")
triple5
Harry is not cold.
False
1
inv-proof
[(triple7)]
("Harry" "is" "cold" "-")
triple7
Gary is red.
True
2
proof
[(((triple5) -> rule3))]
("Gary" "is" "red" "+")
((triple5) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Anne is not cold.
False
2
inv-proof
[(((triple1) -> rule7))]
("Anne" "is" "cold" "-")
((triple1) -> (rule7 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Charlie is young.
True
3
proof
[(((((triple3) -> rule7)) -> rule9) OR ((((triple4) -> rule6)) -> rule9) OR ((((((triple2) -> rule3)) -> rule6)) -> rule9))]
("Charlie" "is" "young" "+")
((((triple3) -> (rule7 % int2))) -> (rule9 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple4) -> (rule6 % int2))) -> (rule9 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Anne is not young.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule9))]
("Anne" "is" "young" "-")
((((triple1) -> (rule7 % int2))) -> (rule9 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Gary is young.
True
4
proof
[(((((((triple5) -> rule3)) -> rule6)) -> rule9))]
("Gary" "is" "young" "+")
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Anne is not blue.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule9)) -> rule1))]
("Anne" "is" "blue" "-")
((((((triple1) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is red.
True
5
proof
[(((((((((triple1) -> rule7)) -> rule9)) -> rule1)) -> rule3))]
("Anne" "is" "red" "+")
((((((((triple1) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Harry is not white.
False
8
inv-proof
[(((((((((triple7) -> rule9)) -> rule1)) -> rule3) ((((triple7) -> rule9)) -> rule1)) -> rule5))]
("Harry" "is" "white" "-")
((((((((triple7) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) ((((triple7) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Anne is white.
True
10
proof
[(((((((((((triple1) -> rule7)) -> rule9)) -> rule1)) -> rule3) ((((((triple1) -> rule7)) -> rule9)) -> rule1)) -> rule5))]
("Anne" "is" "white" "+")
((((((((((triple1) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) ((((((triple1) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
int5
Anne is not white.
False
10
inv-proof
[(((((((((((triple1) -> rule7)) -> rule9)) -> rule1)) -> rule3) ((((((triple1) -> rule7)) -> rule9)) -> rule1)) -> rule5))]
("Anne" "is" "white" "-")
((((((((((triple1) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) ((((((triple1) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
int5
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is nice.[(triple1)] Charlie is blue.[(triple2 OR ((((((triple3) -> rule7)) -> rule9)) -> rule1) OR ((((((triple4) -> rule6)) -> rule9)) -> rule1))] Charlie is nice.[(triple3)] Charlie is red.[(triple4 OR ((triple2) -> rule3) OR ((((((((triple3) -> rule7)) -> rule9)) -> rule1)) -> rule3))] Gary is blue.[(triple5)] Gary is white.[(triple6 OR ((((triple5) -> rule3) triple5) -> rule5))] Harry is cold.[(triple7)] @1: Anne is cold.[(((triple1) -> rule7))] Charlie is cold.[(((triple3) -> rule7) OR ((triple4) -> rule6) OR ((((triple2) -> rule3)) -> rule6))] Charlie is white.[(((triple4 triple2) -> rule5) OR ((((triple2) -> rule3) triple2) -> rule5) OR ((triple4 ((((((triple3) -> rule7)) -> rule9)) -> rule1)) -> rule5) OR ((triple4 ((((((triple4) -> rule6)) -> rule9)) -> rule1)) -> rule5) OR ((((triple2) -> rule3) ((((((triple3) -> rule7)) -> rule9)) -> rule1)) -> rule5) OR ((((triple2) -> rule3) ((((((triple4) -> rule6)) -> rule9)) -> rule1)) -> rule5) OR ((((((((((triple3) -> rule7)) -> rule9)) -> rule1)) -> rule3) triple2) -> rule5) OR ((((((((((triple3) -> rule7)) -> rule9)) -> rule1)) -> rule3) ((((((triple3) -> rule7)) -> rule9)) -> rule1)) -> rule5) OR ((((((((((triple3) -> rule7)) -> rule9)) -> rule1)) -> rule3) ((((((triple4) -> rule6)) -> rule9)) -> rule1)) -> rule5))] Gary is red.[(((triple5) -> rule3))] Harry is young.[(((triple7) -> rule9))] @2: Anne is young.[(((((triple1) -> rule7)) -> rule9))] Charlie is young.[(((((triple3) -> rule7)) -> rule9) OR ((((triple4) -> rule6)) -> rule9) OR ((((((triple2) -> rule3)) -> rule6)) -> rule9))] Gary is cold.[(((((triple5) -> rule3)) -> rule6))] Harry is blue.[(((((triple7) -> rule9)) -> rule1))] @3: Anne is blue.[(((((((triple1) -> rule7)) -> rule9)) -> rule1))] Gary is young.[(((((((triple5) -> rule3)) -> rule6)) -> rule9))] Harry is red.[(((((((triple7) -> rule9)) -> rule1)) -> rule3))] @4: Anne is red.[(((((((((triple1) -> rule7)) -> rule9)) -> rule1)) -> rule3))] Harry is white.[(((((((((triple7) -> rule9)) -> rule1)) -> rule3) ((((triple7) -> rule9)) -> rule1)) -> rule5))] @5: Anne is white.[(((((((((((triple1) -> rule7)) -> rule9)) -> rule1)) -> rule3) ((((((triple1) -> rule7)) -> rule9)) -> rule1)) -> rule5))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
((((((triple3) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((((triple4) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
((triple2) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((((((triple3) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
Gary is white.
("Gary" "is" "white" "+")
triple6
((((triple5) -> (rule3 % int2)) triple5) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule7 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3) -> (rule7 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple4) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((triple4 triple2) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple2) -> (rule3 % int2)) triple2) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((triple4 ((((((triple3) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
((triple4 ((((((triple4) -> (rule6 % int4))) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
((((triple2) -> (rule3 % int5)) ((((((triple3) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Charlie is red.
("Charlie" "is" "red" "+")
int5
((((triple2) -> (rule3 % int5)) ((((((triple4) -> (rule6 % int4))) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Charlie is red.
("Charlie" "is" "red" "+")
int5
((((((((((triple3) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) triple2) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is cold.
("Charlie" "is" "cold" "+")
int5
((((((((((triple3) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) ((((((triple3) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is cold.
("Charlie" "is" "cold" "+")
int5
((((((((((triple3) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) ((((((triple4) -> (rule6 % int5))) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is cold.
("Charlie" "is" "cold" "+")
int5
Gary is red.
("Gary" "is" "red" "+")
((triple5) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple7) -> (rule9 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule7 % int2))) -> (rule9 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((((triple3) -> (rule7 % int2))) -> (rule9 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple4) -> (rule6 % int2))) -> (rule9 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((triple7) -> (rule9 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((((((triple1) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
((((((triple7) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
((((((((triple1) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Harry is white.
("Harry" "is" "white" "+")
((((((((triple7) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) ((((triple7) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
((((((((((triple1) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) ((((((triple1) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
int5