Anne is round. Charlie is round. Charlie is young. Cold, nice people are green. All round people are red. Cold people are nice. If someone is round and red then they are cold. Young people are cold. All green, cold people are round.
Anne is round.
("Anne" "is" "round" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Cold, nice people are green.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
All round people are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone is round and red then they are cold.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
All green, cold people are round.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
Charlie is round.
True
1
proof
[(triple2 OR ((((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule3)) -> rule1) ((triple3) -> rule5)) -> rule6))]
("Charlie" "is" "round" "+")
triple2
((((((triple3) -> (rule5 % int4)) ((((triple3) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule1 % int2)) ((triple3) -> (rule5 % int4))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Charlie is not round.
False
1
inv-proof
[(triple2 OR ((((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule3)) -> rule1) ((triple3) -> rule5)) -> rule6))]
("Charlie" "is" "round" "-")
triple2
((((((triple3) -> (rule5 % int4)) ((((triple3) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule1 % int2)) ((triple3) -> (rule5 % int4))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Charlie is red.
True
2
proof
[(((triple2) -> rule2) OR ((((((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule3)) -> rule1) ((triple3) -> rule5)) -> rule6)) -> rule2))]
("Charlie" "is" "red" "+")
((triple2) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((((((triple3) -> (rule5 % int5)) ((((triple3) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule1 % int3)) ((triple3) -> (rule5 % int5))) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is cold.
("Charlie" "is" "cold" "+")
int5
Charlie is not cold.
False
2
inv-proof
[(((triple3) -> rule5) OR ((triple2 ((triple2) -> rule2)) -> rule4))]
("Charlie" "is" "cold" "-")
((triple3) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple2 ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is nice.
True
3
proof
[(((((triple3) -> rule5)) -> rule3) OR ((((triple2 ((triple2) -> rule2)) -> rule4)) -> rule3))]
("Charlie" "is" "nice" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Anne is not cold.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule4))]
("Anne" "is" "cold" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is nice.
True
5
proof
[(((((triple1 ((triple1) -> rule2)) -> rule4)) -> rule3))]
("Anne" "is" "nice" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Charlie is not green.
False
6
inv-proof
[(((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule3)) -> rule1) OR ((((triple2 ((triple2) -> rule2)) -> rule4) ((((triple3) -> rule5)) -> rule3)) -> rule1) OR ((((triple3) -> rule5) ((((triple2 ((triple2) -> rule2)) -> rule4)) -> rule3)) -> rule1) OR ((((triple2 ((triple2) -> rule2)) -> rule4) ((((triple2 ((triple2) -> rule2)) -> rule4)) -> rule3)) -> rule1))]
("Charlie" "is" "green" "-")
((((triple3) -> (rule5 % int3)) ((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((triple2 ((triple2) -> (rule2 % int4))) -> (rule4 % int3)) ((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
((((triple3) -> (rule5 % int4)) ((((triple2 ((triple2) -> (rule2 % int3))) -> (rule4 % int4))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
((((triple2 ((triple2) -> (rule2 % int4))) -> (rule4 % int3)) ((((triple2 ((triple2) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is round.[(triple1)] Charlie is round.[(triple2 OR ((((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule3)) -> rule1) ((triple3) -> rule5)) -> rule6))] Charlie is young.[(triple3)] @1: Anne is red.[(((triple1) -> rule2))] Charlie is cold.[(((triple3) -> rule5) OR ((triple2 ((triple2) -> rule2)) -> rule4))] Charlie is red.[(((triple2) -> rule2) OR ((((((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule3)) -> rule1) ((triple3) -> rule5)) -> rule6)) -> rule2))] @2: Anne is cold.[(((triple1 ((triple1) -> rule2)) -> rule4))] Charlie is nice.[(((((triple3) -> rule5)) -> rule3) OR ((((triple2 ((triple2) -> rule2)) -> rule4)) -> rule3))] @3: Anne is nice.[(((((triple1 ((triple1) -> rule2)) -> rule4)) -> rule3))] Charlie is green.[(((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule3)) -> rule1) OR ((((triple2 ((triple2) -> rule2)) -> rule4) ((((triple3) -> rule5)) -> rule3)) -> rule1) OR ((((triple3) -> rule5) ((((triple2 ((triple2) -> rule2)) -> rule4)) -> rule3)) -> rule1) OR ((((triple2 ((triple2) -> rule2)) -> rule4) ((((triple2 ((triple2) -> rule2)) -> rule4)) -> rule3)) -> rule1))] @4: Anne is green.[(((((triple1 ((triple1) -> rule2)) -> rule4) ((((triple1 ((triple1) -> rule2)) -> rule4)) -> rule3)) -> rule1))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
((((((triple3) -> (rule5 % int4)) ((((triple3) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule1 % int2)) ((triple3) -> (rule5 % int4))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple2 ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((triple2) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((((((triple3) -> (rule5 % int5)) ((((triple3) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule1 % int3)) ((triple3) -> (rule5 % int5))) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is cold.
("Charlie" "is" "cold" "+")
int5
Anne is cold.
("Anne" "is" "cold" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
((((triple3) -> (rule5 % int3)) ((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((triple2 ((triple2) -> (rule2 % int4))) -> (rule4 % int3)) ((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
((((triple3) -> (rule5 % int4)) ((((triple2 ((triple2) -> (rule2 % int3))) -> (rule4 % int4))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
((((triple2 ((triple2) -> (rule2 % int4))) -> (rule4 % int3)) ((((triple2 ((triple2) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
((((triple1 ((triple1) -> (rule2 % int4))) -> (rule4 % int3)) ((((triple1 ((triple1) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4