Bob is blue. Bob is cold. Bob is quiet. Bob is rough. Bob is white. Erin is cold. Erin is quiet. Erin is red. Gary is big. Gary is rough. Red things are blue. All red things are cold. If something is quiet then it is big. If something is rough and quiet then it is big. If something is rough and big then it is red. If Gary is blue and Gary is rough then Gary is cold.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
All red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something is quiet then it is big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If something is rough and quiet then it is big.
((("something" "is" "rough" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If something is rough and big then it is red.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If Gary is blue and Gary is rough then Gary is cold.
((("Gary" "is" "blue" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "cold" "+"))
Bob is white.
True
1
proof
[(triple5)]
("Bob" "is" "white" "+")
triple5
Gary is not big.
False
1
inv-proof
[(triple9)]
("Gary" "is" "big" "-")
triple9
Gary is red.
True
3
proof
[(((triple10 triple9) -> rule5))]
("Gary" "is" "red" "+")
((triple10 triple9) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple8) -> rule1))]
("Erin" "is" "blue" "-")
((triple8) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Gary is blue.
True
4
proof
[(((((triple10 triple9) -> rule5)) -> rule1))]
("Gary" "is" "blue" "+")
((((triple10 triple9) -> (rule5 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not cold.
False
4
inv-proof
[(((((triple10 triple9) -> rule5)) -> rule2) OR ((((((triple10 triple9) -> rule5)) -> rule1) triple10) -> rule6))]
("Gary" "is" "cold" "-")
((((triple10 triple9) -> (rule5 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple10 triple9) -> (rule5 % int3))) -> (rule1 % int2)) triple10) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Bob is blue.[(triple1 OR ((((triple4 ((triple3) -> rule3)) -> rule5)) -> rule1) OR ((((triple4 ((triple4 triple3) -> rule4)) -> rule5)) -> rule1))] Bob is cold.[(triple2 OR ((((triple4 ((triple3) -> rule3)) -> rule5)) -> rule2) OR ((((triple4 ((triple4 triple3) -> rule4)) -> rule5)) -> rule2))] Bob is quiet.[(triple3)] Bob is rough.[(triple4)] Bob is white.[(triple5)] Erin is cold.[(triple6 OR ((triple8) -> rule2))] Erin is quiet.[(triple7)] Erin is red.[(triple8)] Gary is big.[(triple9)] Gary is rough.[(triple10)] @1: Bob is big.[(((triple3) -> rule3) OR ((triple4 triple3) -> rule4))] Erin is big.[(((triple7) -> rule3))] Erin is blue.[(((triple8) -> rule1))] Gary is red.[(((triple10 triple9) -> rule5))] @2: Bob is red.[(((triple4 ((triple3) -> rule3)) -> rule5) OR ((triple4 ((triple4 triple3) -> rule4)) -> rule5))] Gary is blue.[(((((triple10 triple9) -> rule5)) -> rule1))] Gary is cold.[(((((triple10 triple9) -> rule5)) -> rule2) OR ((((((triple10 triple9) -> rule5)) -> rule1) triple10) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((((triple4 ((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((triple4 ((triple4 triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((((triple4 ((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((triple4 ((triple4 triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Erin is cold.
("Erin" "is" "cold" "+")
triple6
((triple8) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Erin is red.
("Erin" "is" "red" "+")
triple8
Gary is big.
("Gary" "is" "big" "+")
triple9
Gary is rough.
("Gary" "is" "rough" "+")
triple10
Bob is big.
("Bob" "is" "big" "+")
((triple3) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple4 triple3) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple7) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple8) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple10 triple9) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple4 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((triple4 ((triple4 triple3) -> (rule4 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((triple10 triple9) -> (rule5 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((triple10 triple9) -> (rule5 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple10 triple9) -> (rule5 % int3))) -> (rule1 % int2)) triple10) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3