Anne is not big. Anne is blue. Anne is red. Charlie is big. Charlie is red. Charlie is white. Gary is not blue. Gary is green. Gary is red. Gary is white. Gary is young. Harry is red. If Anne is young then Anne is cold. Young people are cold. If someone is red then they are cold. All cold people are young. If Anne is green and Anne is cold then Anne is white. White people are red. Young people are white. All young people are green.
Anne is not big.
("Anne" "is" "big" "-")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is red.
("Anne" "is" "red" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is red.
("Harry" "is" "red" "+")
If Anne is young then Anne is cold.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "cold" "+"))
Young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
All cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If Anne is green and Anne is cold then Anne is white.
((("Anne" "is" "green" "+") ("Anne" "is" "cold" "+")) -> ("Anne" "is" "white" "+"))
White people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Young people are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
All young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Gary is white.
True
1
proof
[(triple10 OR ((triple11) -> rule7) OR ((((((triple9) -> rule3)) -> rule4)) -> rule7))]
("Gary" "is" "white" "+")
triple10
((triple11) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((((triple9) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is not young.
False
1
inv-proof
[(triple11 OR ((((triple9) -> rule3)) -> rule4) OR ((((((triple10) -> rule6)) -> rule3)) -> rule4))]
("Gary" "is" "young" "-")
triple11
((((triple9) -> (rule3 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((((triple10) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is cold.
True
2
proof
[(((triple11) -> rule2) OR ((triple9) -> rule3) OR ((((triple10) -> rule6)) -> rule3) OR ((((((triple11) -> rule7)) -> rule6)) -> rule3))]
("Gary" "is" "cold" "+")
((triple11) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple9) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple11) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not cold.
False
2
inv-proof
[(((triple11) -> rule2) OR ((triple9) -> rule3) OR ((((triple10) -> rule6)) -> rule3) OR ((((((triple11) -> rule7)) -> rule6)) -> rule3))]
("Gary" "is" "cold" "-")
((triple11) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple9) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple11) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Anne is young.
True
3
proof
[(((((triple3) -> rule3)) -> rule4))]
("Anne" "is" "young" "+")
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not young.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule4))]
("Anne" "is" "young" "-")
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is white.
True
4
proof
[(((((((triple3) -> rule3)) -> rule4)) -> rule7) OR ((((((((triple3) -> rule3)) -> rule4)) -> rule8) ((triple3) -> rule3)) -> rule5))]
("Anne" "is" "white" "+")
((((((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((((((triple3) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) ((triple3) -> (rule3 % int4))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Charlie is not green.
False
4
inv-proof
[(((((((triple5) -> rule3)) -> rule4)) -> rule8) OR ((((((((triple6) -> rule6)) -> rule3)) -> rule4)) -> rule8))]
("Charlie" "is" "green" "-")
((((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((((((triple6) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Anne is blue.[(triple2)] Anne is not big.[(triple1)] Anne is red.[(triple3)] Charlie is big.[(triple4)] Charlie is red.[(triple5 OR ((triple6) -> rule6))] Charlie is white.[(triple6 OR ((((((triple5) -> rule3)) -> rule4)) -> rule7))] Gary is green.[(triple8 OR ((triple11) -> rule8) OR ((((((triple9) -> rule3)) -> rule4)) -> rule8) OR ((((((((triple10) -> rule6)) -> rule3)) -> rule4)) -> rule8))] Gary is not blue.[(triple7)] Gary is red.[(triple9 OR ((triple10) -> rule6) OR ((((triple11) -> rule7)) -> rule6))] Gary is white.[(triple10 OR ((triple11) -> rule7) OR ((((((triple9) -> rule3)) -> rule4)) -> rule7))] Gary is young.[(triple11 OR ((((triple9) -> rule3)) -> rule4) OR ((((((triple10) -> rule6)) -> rule3)) -> rule4))] Harry is red.[(triple12)] @1: Anne is cold.[(((triple3) -> rule3))] Charlie is cold.[(((triple5) -> rule3) OR ((((triple6) -> rule6)) -> rule3))] Gary is cold.[(((triple11) -> rule2) OR ((triple9) -> rule3) OR ((((triple10) -> rule6)) -> rule3) OR ((((((triple11) -> rule7)) -> rule6)) -> rule3))] Harry is cold.[(((triple12) -> rule3))] @2: Anne is young.[(((((triple3) -> rule3)) -> rule4))] Charlie is young.[(((((triple5) -> rule3)) -> rule4) OR ((((((triple6) -> rule6)) -> rule3)) -> rule4))] Harry is young.[(((((triple12) -> rule3)) -> rule4))] @3: Anne is green.[(((((((triple3) -> rule3)) -> rule4)) -> rule8))] Anne is white.[(((((((triple3) -> rule3)) -> rule4)) -> rule7) OR ((((((((triple3) -> rule3)) -> rule4)) -> rule8) ((triple3) -> rule3)) -> rule5))] Charlie is green.[(((((((triple5) -> rule3)) -> rule4)) -> rule8) OR ((((((((triple6) -> rule6)) -> rule3)) -> rule4)) -> rule8))] Harry is green.[(((((((triple12) -> rule3)) -> rule4)) -> rule8))] Harry is white.[(((((((triple12) -> rule3)) -> rule4)) -> rule7))]
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is not big.
("Anne" "is" "big" "-")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
((triple6) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple6
((((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
triple8
((triple11) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((((triple9) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((((((triple10) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is not blue.
("Gary" "is" "blue" "-")
triple7
Gary is red.
("Gary" "is" "red" "+")
triple9
((triple10) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple11) -> (rule7 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
triple10
((triple11) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((((triple9) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
triple11
((((triple9) -> (rule3 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((((triple10) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % 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" "+")
triple12
Anne is cold.
("Anne" "is" "cold" "+")
((triple3) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple5) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((triple11) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple9) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple11) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
((triple12) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
((((triple12) -> (rule3 % int2))) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((((((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
((((((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((((((triple3) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) ((triple3) -> (rule3 % int4))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Charlie is green.
("Charlie" "is" "green" "+")
((((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((((((triple6) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Harry is green.
("Harry" "is" "green" "+")
((((((triple12) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((((((triple12) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3