Anne is blue. Anne is red. Bob is blue. Bob is cold. Charlie is kind. Charlie is red. Erin is blue. Erin is cold. Erin is quiet. Erin is white. If something is quiet then it is furry. If Anne is cold then Anne is kind. Kind things are red. Red things are white. Red things are kind. Blue, white things are kind. If something is red then it is furry. If something is furry then it is quiet. Cold things are white.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
If something is quiet then it is furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If Anne is cold then Anne is kind.
((("Anne" "is" "cold" "+")) -> ("Anne" "is" "kind" "+"))
Kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
Red things are white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
Red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Blue, white things are kind.
((("something" "is" "blue" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
If something is red then it is furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If something is furry then it is quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Cold things are white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Bob is blue.
True
1
proof
[(triple3)]
("Bob" "is" "blue" "+")
triple3
Charlie is not kind.
False
1
inv-proof
[(triple5 OR ((triple6) -> rule5))]
("Charlie" "is" "kind" "-")
triple5
((triple6) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Erin is kind.
True
3
proof
[(((triple7 triple10) -> rule6) OR ((triple7 ((triple8) -> rule9)) -> rule6))]
("Erin" "is" "kind" "+")
((triple7 triple10) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple7 ((triple8) -> (rule9 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Charlie is not white.
False
2
inv-proof
[(((triple6) -> rule4) OR ((((triple5) -> rule3)) -> rule4))]
("Charlie" "is" "white" "-")
((triple6) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Erin is red.
True
4
proof
[(((((triple7 triple10) -> rule6)) -> rule3) OR ((((triple7 ((triple8) -> rule9)) -> rule6)) -> rule3))]
("Erin" "is" "red" "+")
((((triple7 triple10) -> (rule6 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple7 ((triple8) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Bob is not kind.
False
4
inv-proof
[(((triple3 ((triple4) -> rule9)) -> rule6))]
("Bob" "is" "kind" "-")
((triple3 ((triple4) -> (rule9 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is red.
True
5
proof
[(((((triple3 ((triple4) -> rule9)) -> rule6)) -> rule3))]
("Bob" "is" "red" "+")
((((triple3 ((triple4) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not red.
False
5
inv-proof
[(((((triple3 ((triple4) -> rule9)) -> rule6)) -> rule3))]
("Bob" "is" "red" "-")
((((triple3 ((triple4) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is furry.
True
6
proof
[(((((((triple3 ((triple4) -> rule9)) -> rule6)) -> rule3)) -> rule7))]
("Bob" "is" "furry" "+")
((((((triple3 ((triple4) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is not furry.
False
6
inv-proof
[(((((((triple3 ((triple4) -> rule9)) -> rule6)) -> rule3)) -> rule7))]
("Bob" "is" "furry" "-")
((((((triple3 ((triple4) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is quiet.
True
7
proof
[(((((((((triple3 ((triple4) -> rule9)) -> rule6)) -> rule3)) -> rule7)) -> rule8))]
("Bob" "is" "quiet" "+")
((((((((triple3 ((triple4) -> (rule9 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5
Bob is not quiet.
False
7
inv-proof
[(((((((((triple3 ((triple4) -> rule9)) -> rule6)) -> rule3)) -> rule7)) -> rule8))]
("Bob" "is" "quiet" "-")
((((((((triple3 ((triple4) -> (rule9 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Anne is blue.[(triple1)] Anne is red.[(triple2)] Bob is blue.[(triple3)] Bob is cold.[(triple4)] Charlie is kind.[(triple5 OR ((triple6) -> rule5))] Charlie is red.[(triple6 OR ((triple5) -> rule3))] Erin is blue.[(triple7)] Erin is cold.[(triple8)] Erin is quiet.[(triple9 OR ((((((((triple7 triple10) -> rule6)) -> rule3)) -> rule7)) -> rule8) OR ((((((((triple7 ((triple8) -> rule9)) -> rule6)) -> rule3)) -> rule7)) -> rule8))] Erin is white.[(triple10 OR ((triple8) -> rule9))] @1: Anne is furry.[(((triple2) -> rule7))] Anne is kind.[(((triple2) -> rule5) OR ((triple1 ((triple2) -> rule4)) -> rule6))] Anne is white.[(((triple2) -> rule4))] Bob is white.[(((triple4) -> rule9))] Charlie is furry.[(((triple6) -> rule7) OR ((((triple5) -> rule3)) -> rule7))] Charlie is white.[(((triple6) -> rule4) OR ((((triple5) -> rule3)) -> rule4))] Erin is furry.[(((triple9) -> rule1) OR ((((((triple7 triple10) -> rule6)) -> rule3)) -> rule7) OR ((((((triple7 ((triple8) -> rule9)) -> rule6)) -> rule3)) -> rule7))] Erin is kind.[(((triple7 triple10) -> rule6) OR ((triple7 ((triple8) -> rule9)) -> rule6))] @2: Anne is quiet.[(((((triple2) -> rule7)) -> rule8))] Bob is kind.[(((triple3 ((triple4) -> rule9)) -> rule6))] Charlie is quiet.[(((((triple6) -> rule7)) -> rule8) OR ((((((triple5) -> rule3)) -> rule7)) -> rule8))] Erin is red.[(((((triple7 triple10) -> rule6)) -> rule3) OR ((((triple7 ((triple8) -> rule9)) -> rule6)) -> rule3))] @3: Bob is red.[(((((triple3 ((triple4) -> rule9)) -> rule6)) -> rule3))] @4: Bob is furry.[(((((((triple3 ((triple4) -> rule9)) -> rule6)) -> rule3)) -> rule7))] @5: Bob is quiet.[(((((((((triple3 ((triple4) -> rule9)) -> rule6)) -> rule3)) -> rule7)) -> rule8))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
((triple6) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple6
((triple5) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
triple8
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
((((((((triple7 triple10) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
((((((((triple7 ((triple8) -> (rule9 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5
Erin is white.
("Erin" "is" "white" "+")
triple10
((triple8) -> (rule9 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((triple2) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple2) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple1 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((triple2) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple4) -> (rule9 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple6) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((triple6) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((triple9) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((((triple7 triple10) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple7 ((triple8) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
((triple7 triple10) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple7 ((triple8) -> (rule9 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((triple3 ((triple4) -> (rule9 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple6) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
((((triple7 triple10) -> (rule6 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple7 ((triple8) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
((((triple3 ((triple4) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
((((((triple3 ((triple4) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
((((((((triple3 ((triple4) -> (rule9 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5