Anne is cold. Charlie is cold. Charlie is quiet. Charlie is red. Charlie is round. Gary is cold. Gary is red. Gary is round. Gary is young. Harry is red. Harry is round. Harry is young. If something is round then it is white. If something is cold then it is smart. If something is red and smart then it is cold. If something is round then it is cold. Smart, young things are round. Smart things are red. Red things are young.
Anne is cold.
("Anne" "is" "cold" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is round then it is white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If something is cold then it is smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If something is red and smart then it is cold.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
If something is round then it is cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
Smart, young things are round.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
Smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Gary is young.
True
1
proof
[(triple9 OR ((triple7) -> rule7) OR ((((((triple6) -> rule2)) -> rule6)) -> rule7) OR ((((((((triple8) -> rule4)) -> rule2)) -> rule6)) -> rule7))]
("Gary" "is" "young" "+")
triple9
((triple7) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((((triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((((((triple8) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Charlie is not quiet.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "quiet" "-")
triple3
Charlie is smart.
True
2
proof
[(((triple2) -> rule2) OR ((((triple5) -> rule4)) -> rule2))]
("Charlie" "is" "smart" "+")
((triple2) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Harry is not white.
False
2
inv-proof
[(((triple11) -> rule1))]
("Harry" "is" "white" "-")
((triple11) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
True
3
proof
[(((((triple11) -> rule4)) -> rule2))]
("Harry" "is" "smart" "+")
((((triple11) -> (rule4 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Anne is not red.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule6))]
("Anne" "is" "red" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is young.
True
4
proof
[(((((((triple1) -> rule2)) -> rule6)) -> rule7))]
("Anne" "is" "young" "+")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not young.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule6)) -> rule7))]
("Anne" "is" "young" "-")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is round.
True
7
proof
[(((((triple1) -> rule2) ((((((triple1) -> rule2)) -> rule6)) -> rule7)) -> rule5))]
("Anne" "is" "round" "+")
((((triple1) -> (rule2 % int4)) ((((((triple1) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is not round.
False
7
inv-proof
[(((((triple1) -> rule2) ((((((triple1) -> rule2)) -> rule6)) -> rule7)) -> rule5))]
("Anne" "is" "round" "-")
((((triple1) -> (rule2 % int4)) ((((((triple1) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is white.
True
8
proof
[(((((((triple1) -> rule2) ((((((triple1) -> rule2)) -> rule6)) -> rule7)) -> rule5)) -> rule1))]
("Anne" "is" "white" "+")
((((((triple1) -> (rule2 % int5)) ((((((triple1) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
int5
Anne is not white.
False
8
inv-proof
[(((((((triple1) -> rule2) ((((((triple1) -> rule2)) -> rule6)) -> rule7)) -> rule5)) -> rule1))]
("Anne" "is" "white" "-")
((((((triple1) -> (rule2 % int5)) ((((((triple1) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
int5
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Anne is cold.[(triple1)] Charlie is cold.[(triple2 OR ((triple5) -> rule4))] Charlie is quiet.[(triple3)] Charlie is red.[(triple4 OR ((((triple2) -> rule2)) -> rule6) OR ((((((triple5) -> rule4)) -> rule2)) -> rule6))] Charlie is round.[(triple5 OR ((((triple2) -> rule2) ((triple4) -> rule7)) -> rule5) OR ((((triple2) -> rule2) ((((((triple2) -> rule2)) -> rule6)) -> rule7)) -> rule5))] Gary is cold.[(triple6 OR ((triple8) -> rule4))] Gary is red.[(triple7 OR ((((triple6) -> rule2)) -> rule6) OR ((((((triple8) -> rule4)) -> rule2)) -> rule6))] Gary is round.[(triple8 OR ((((triple6) -> rule2) triple9) -> rule5) OR ((((triple6) -> rule2) ((triple7) -> rule7)) -> rule5) OR ((((triple6) -> rule2) ((((((triple6) -> rule2)) -> rule6)) -> rule7)) -> rule5))] Gary is young.[(triple9 OR ((triple7) -> rule7) OR ((((((triple6) -> rule2)) -> rule6)) -> rule7) OR ((((((((triple8) -> rule4)) -> rule2)) -> rule6)) -> rule7))] Harry is red.[(triple10 OR ((((((triple11) -> rule4)) -> rule2)) -> rule6))] Harry is round.[(triple11)] Harry is young.[(triple12 OR ((triple10) -> rule7) OR ((((((((triple11) -> rule4)) -> rule2)) -> rule6)) -> rule7))] @1: Anne is smart.[(((triple1) -> rule2))] Charlie is smart.[(((triple2) -> rule2) OR ((((triple5) -> rule4)) -> rule2))] Charlie is white.[(((triple5) -> rule1) OR ((((((triple2) -> rule2) ((triple4) -> rule7)) -> rule5)) -> rule1) OR ((((((triple2) -> rule2) ((((((triple2) -> rule2)) -> rule6)) -> rule7)) -> rule5)) -> rule1))] Charlie is young.[(((triple4) -> rule7) OR ((((((triple2) -> rule2)) -> rule6)) -> rule7) OR ((((((((triple5) -> rule4)) -> rule2)) -> rule6)) -> rule7))] Gary is smart.[(((triple6) -> rule2) OR ((((triple8) -> rule4)) -> rule2))] Gary is white.[(((triple8) -> rule1) OR ((((((triple6) -> rule2) triple9) -> rule5)) -> rule1) OR ((((((triple6) -> rule2) ((triple7) -> rule7)) -> rule5)) -> rule1) OR ((((((triple6) -> rule2) ((((((triple6) -> rule2)) -> rule6)) -> rule7)) -> rule5)) -> rule1))] Harry is cold.[(((triple11) -> rule4))] Harry is white.[(((triple11) -> rule1))] @2: Anne is red.[(((((triple1) -> rule2)) -> rule6))] Harry is smart.[(((((triple11) -> rule4)) -> rule2))] @3: Anne is young.[(((((((triple1) -> rule2)) -> rule6)) -> rule7))] @4: Anne is round.[(((((triple1) -> rule2) ((((((triple1) -> rule2)) -> rule6)) -> rule7)) -> rule5))] @5: Anne is white.[(((((((triple1) -> rule2) ((((((triple1) -> rule2)) -> rule6)) -> rule7)) -> rule5)) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((triple5) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
((((((triple5) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
triple5
((((triple2) -> (rule2 % int3)) ((triple4) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((triple2) -> (rule2 % int4)) ((((((triple2) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
triple6
((triple8) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple7
((((triple6) -> (rule2 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((((triple8) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
triple8
((((triple6) -> (rule2 % int2)) triple9) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple6) -> (rule2 % int3)) ((triple7) -> (rule7 % int2))) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((triple6) -> (rule2 % int4)) ((((((triple6) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is young.
("Gary" "is" "young" "+")
triple9
((triple7) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((((triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((((((triple8) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Harry is red.
("Harry" "is" "red" "+")
triple10
((((((triple11) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
((triple10) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((((((triple11) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((triple5) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((((triple2) -> (rule2 % int4)) ((triple4) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
((((((triple2) -> (rule2 % int5)) ((((((triple2) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Charlie is smart.
("Charlie" "is" "smart" "+")
int5
Charlie is young.
("Charlie" "is" "young" "+")
((triple4) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((((((triple5) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
((triple6) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple8) -> (rule4 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((triple8) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((((triple6) -> (rule2 % int3)) triple9) -> (rule5 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((((triple6) -> (rule2 % int4)) ((triple7) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
((((((triple6) -> (rule2 % int5)) ((((((triple6) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Harry is cold.
("Harry" "is" "cold" "+")
((triple11) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple11) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((triple11) -> (rule4 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
((((triple1) -> (rule2 % int4)) ((((((triple1) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
((((((triple1) -> (rule2 % int5)) ((((((triple1) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
int5