Bob is cold. Bob is furry. Bob is smart. Bob is white. Charlie is furry. Erin is green. Erin is quiet. Erin is white. Gary is furry. Gary is quiet. Furry people are white. If someone is quiet then they are cold. If someone is white and round then they are quiet. If someone is white then they are round. If Charlie is cold and Charlie is furry then Charlie is green.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If someone is quiet then they are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If someone is white and round then they are quiet.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If someone is white then they are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If Charlie is cold and Charlie is furry then Charlie is green.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "green" "+"))
Gary is quiet.
True
1
proof
[(triple10 OR ((((triple9) -> rule1) ((((triple9) -> rule1)) -> rule4)) -> rule3))]
("Gary" "is" "quiet" "+")
triple10
((((triple9) -> (rule1 % int3)) ((((triple9) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not quiet.
False
1
inv-proof
[(triple10 OR ((((triple9) -> rule1) ((((triple9) -> rule1)) -> rule4)) -> rule3))]
("Gary" "is" "quiet" "-")
triple10
((((triple9) -> (rule1 % int3)) ((((triple9) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Charlie is white.
True
2
proof
[(((triple5) -> rule1))]
("Charlie" "is" "white" "+")
((triple5) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple10) -> rule2) OR ((((((triple9) -> rule1) ((((triple9) -> rule1)) -> rule4)) -> rule3)) -> rule2))]
("Gary" "is" "cold" "-")
((triple10) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((((triple9) -> (rule1 % int4)) ((((triple9) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Charlie is round.
True
3
proof
[(((((triple5) -> rule1)) -> rule4))]
("Charlie" "is" "round" "+")
((((triple5) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Gary is not round.
False
3
inv-proof
[(((((triple9) -> rule1)) -> rule4))]
("Gary" "is" "round" "-")
((((triple9) -> (rule1 % int2))) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Charlie is quiet.
True
6
proof
[(((((triple5) -> rule1) ((((triple5) -> rule1)) -> rule4)) -> rule3))]
("Charlie" "is" "quiet" "+")
((((triple5) -> (rule1 % int3)) ((((triple5) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not quiet.
False
6
inv-proof
[(((((triple5) -> rule1) ((((triple5) -> rule1)) -> rule4)) -> rule3))]
("Charlie" "is" "quiet" "-")
((((triple5) -> (rule1 % int3)) ((((triple5) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is cold.
True
7
proof
[(((((((triple5) -> rule1) ((((triple5) -> rule1)) -> rule4)) -> rule3)) -> rule2))]
("Charlie" "is" "cold" "+")
((((((triple5) -> (rule1 % int4)) ((((triple5) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is not cold.
False
7
inv-proof
[(((((((triple5) -> rule1) ((((triple5) -> rule1)) -> rule4)) -> rule3)) -> rule2))]
("Charlie" "is" "cold" "-")
((((((triple5) -> (rule1 % int4)) ((((triple5) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is green.
True
9
proof
[(((((((((triple5) -> rule1) ((((triple5) -> rule1)) -> rule4)) -> rule3)) -> rule2) triple5) -> rule5))]
("Charlie" "is" "green" "+")
((((((((triple5) -> (rule1 % int5)) ((((triple5) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) triple5) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
int5
Charlie is not green.
False
9
inv-proof
[(((((((((triple5) -> rule1) ((((triple5) -> rule1)) -> rule4)) -> rule3)) -> rule2) triple5) -> rule5))]
("Charlie" "is" "green" "-")
((((((((triple5) -> (rule1 % int5)) ((((triple5) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) triple5) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
int5
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Bob is cold.[(triple1 OR ((((triple4 ((triple4) -> rule4)) -> rule3)) -> rule2) OR ((((((triple2) -> rule1) ((triple4) -> rule4)) -> rule3)) -> rule2) OR ((((triple4 ((((triple2) -> rule1)) -> rule4)) -> rule3)) -> rule2) OR ((((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule4)) -> rule3)) -> rule2))] Bob is furry.[(triple2)] Bob is smart.[(triple3)] Bob is white.[(triple4 OR ((triple2) -> rule1))] Charlie is furry.[(triple5)] Erin is green.[(triple6)] Erin is quiet.[(triple7 OR ((triple8 ((triple8) -> rule4)) -> rule3))] Erin is white.[(triple8)] Gary is furry.[(triple9)] Gary is quiet.[(triple10 OR ((((triple9) -> rule1) ((((triple9) -> rule1)) -> rule4)) -> rule3))] @1: Bob is round.[(((triple4) -> rule4) OR ((((triple2) -> rule1)) -> rule4))] Charlie is white.[(((triple5) -> rule1))] Erin is cold.[(((triple7) -> rule2) OR ((((triple8 ((triple8) -> rule4)) -> rule3)) -> rule2))] Erin is round.[(((triple8) -> rule4))] Gary is cold.[(((triple10) -> rule2) OR ((((((triple9) -> rule1) ((((triple9) -> rule1)) -> rule4)) -> rule3)) -> rule2))] Gary is white.[(((triple9) -> rule1))] @2: Bob is quiet.[(((triple4 ((triple4) -> rule4)) -> rule3) OR ((((triple2) -> rule1) ((triple4) -> rule4)) -> rule3) OR ((triple4 ((((triple2) -> rule1)) -> rule4)) -> rule3) OR ((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule4)) -> rule3))] Charlie is round.[(((((triple5) -> rule1)) -> rule4))] Gary is round.[(((((triple9) -> rule1)) -> rule4))] @3: Charlie is quiet.[(((((triple5) -> rule1) ((((triple5) -> rule1)) -> rule4)) -> rule3))] @4: Charlie is cold.[(((((((triple5) -> rule1) ((((triple5) -> rule1)) -> rule4)) -> rule3)) -> rule2))] @5: Charlie is green.[(((((((((triple5) -> rule1) ((((triple5) -> rule1)) -> rule4)) -> rule3)) -> rule2) triple5) -> rule5))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((((triple4 ((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((((triple2) -> (rule1 % int4)) ((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
((((triple4 ((((triple2) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
((((((triple2) -> (rule1 % int4)) ((((triple2) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
((triple2) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
((triple8 ((triple8) -> (rule4 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
triple8
Gary is furry.
("Gary" "is" "furry" "+")
triple9
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
((((triple9) -> (rule1 % int3)) ((((triple9) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
((triple4) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((triple5) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple7) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple8 ((triple8) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
((triple8) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple10) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((((triple9) -> (rule1 % int4)) ((((triple9) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is white.
("Gary" "is" "white" "+")
((triple9) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple4 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple2) -> (rule1 % int3)) ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((triple4 ((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
((((triple5) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((triple9) -> (rule1 % int2))) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple5) -> (rule1 % int3)) ((((triple5) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple5) -> (rule1 % int4)) ((((triple5) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is green.
("Charlie" "is" "green" "+")
((((((((triple5) -> (rule1 % int5)) ((((triple5) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) triple5) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
int5