Anne is furry. Charlie is furry. Charlie is white. If something is furry and kind then it is red. If something is red and green then it is rough. Red things are rough. Furry, red things are rough. If Anne is furry and Anne is kind then Anne is green. If something is quiet then it is kind. If something is furry then it is quiet. If something is furry then it is quiet.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is white.
("Charlie" "is" "white" "+")
If something is furry and kind then it is red.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If something is red and green then it is rough.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Red things are rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Furry, red things are rough.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If Anne is furry and Anne is kind then Anne is green.
((("Anne" "is" "furry" "+") ("Anne" "is" "kind" "+")) -> ("Anne" "is" "green" "+"))
If something is quiet then it is kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If something is furry then it is quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If something is furry then it is quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Charlie is furry.
True
1
proof
[(triple2)]
("Charlie" "is" "furry" "+")
triple2
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Anne is quiet.
True
2
proof
[(((triple1) -> rule7) OR ((triple1) -> rule8))]
("Anne" "is" "quiet" "+")
((triple1) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((triple1) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple2) -> rule7) OR ((triple2) -> rule8))]
("Charlie" "is" "quiet" "-")
((triple2) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple2) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is kind.
True
3
proof
[(((((triple2) -> rule7)) -> rule6) OR ((((triple2) -> rule8)) -> rule6))]
("Charlie" "is" "kind" "+")
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not kind.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule6) OR ((((triple2) -> rule8)) -> rule6))]
("Charlie" "is" "kind" "-")
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Anne is red.
True
5
proof
[(((triple1 ((((triple1) -> rule7)) -> rule6)) -> rule1) OR ((triple1 ((((triple1) -> rule8)) -> rule6)) -> rule1))]
("Anne" "is" "red" "+")
((triple1 ((((triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
((triple1 ((((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is not green.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule7)) -> rule6)) -> rule5) OR ((triple1 ((((triple1) -> rule8)) -> rule6)) -> rule5))]
("Anne" "is" "green" "-")
((triple1 ((((triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
((triple1 ((((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is furry.[(triple1)] Charlie is furry.[(triple2)] Charlie is white.[(triple3)] @1: Anne is quiet.[(((triple1) -> rule7) OR ((triple1) -> rule8))] Charlie is quiet.[(((triple2) -> rule7) OR ((triple2) -> rule8))] @2: Anne is kind.[(((((triple1) -> rule7)) -> rule6) OR ((((triple1) -> rule8)) -> rule6))] Charlie is kind.[(((((triple2) -> rule7)) -> rule6) OR ((((triple2) -> rule8)) -> rule6))] @3: Anne is green.[(((triple1 ((((triple1) -> rule7)) -> rule6)) -> rule5) OR ((triple1 ((((triple1) -> rule8)) -> rule6)) -> rule5))] Anne is red.[(((triple1 ((((triple1) -> rule7)) -> rule6)) -> rule1) OR ((triple1 ((((triple1) -> rule8)) -> rule6)) -> rule1))] Charlie is red.[(((triple2 ((((triple2) -> rule7)) -> rule6)) -> rule1) OR ((triple2 ((((triple2) -> rule8)) -> rule6)) -> rule1))] @4: Anne is rough.[(((((triple1 ((((triple1) -> rule7)) -> rule6)) -> rule1)) -> rule3) OR ((((triple1 ((((triple1) -> rule8)) -> rule6)) -> rule1)) -> rule3) OR ((triple1 ((triple1 ((((triple1) -> rule7)) -> rule6)) -> rule1)) -> rule4) OR ((triple1 ((triple1 ((((triple1) -> rule8)) -> rule6)) -> rule1)) -> rule4) OR ((((triple1 ((((triple1) -> rule7)) -> rule6)) -> rule1) ((triple1 ((((triple1) -> rule7)) -> rule6)) -> rule5)) -> rule2) OR ((((triple1 ((((triple1) -> rule7)) -> rule6)) -> rule1) ((triple1 ((((triple1) -> rule8)) -> rule6)) -> rule5)) -> rule2) OR ((((triple1 ((((triple1) -> rule8)) -> rule6)) -> rule1) ((triple1 ((((triple1) -> rule7)) -> rule6)) -> rule5)) -> rule2) OR ((((triple1 ((((triple1) -> rule8)) -> rule6)) -> rule1) ((triple1 ((((triple1) -> rule8)) -> rule6)) -> rule5)) -> rule2))] Charlie is rough.[(((((triple2 ((((triple2) -> rule7)) -> rule6)) -> rule1)) -> rule3) OR ((((triple2 ((((triple2) -> rule8)) -> rule6)) -> rule1)) -> rule3) OR ((triple2 ((triple2 ((((triple2) -> rule7)) -> rule6)) -> rule1)) -> rule4) OR ((triple2 ((triple2 ((((triple2) -> rule8)) -> rule6)) -> rule1)) -> rule4))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((triple1) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple2) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((triple1 ((((triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
((triple1 ((((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
((triple1 ((((triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
((triple1 ((((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
((triple2 ((((triple2) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((triple2 ((((triple2) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1 ((((triple1) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
((((triple1 ((((triple1) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
((triple1 ((triple1 ((((triple1) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
((triple1 ((triple1 ((((triple1) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
((((triple1 ((((triple1) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((triple1 ((((triple1) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
int5
((((triple1 ((((triple1) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((triple1 ((((triple1) -> (rule8 % int5))) -> (rule6 % int4))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
int5
((((triple1 ((((triple1) -> (rule8 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((triple1 ((((triple1) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
int5
((((triple1 ((((triple1) -> (rule8 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((triple1 ((((triple1) -> (rule8 % int5))) -> (rule6 % int4))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
int5
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple2 ((((triple2) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
((((triple2 ((((triple2) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
((triple2 ((triple2 ((((triple2) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
((triple2 ((triple2 ((((triple2) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4