Bob is blue. Bob is cold. Bob is kind. Bob is white. Dave is blue. Dave is cold. Dave is furry. Dave is kind. Dave is red. Fiona is cold. Fiona is kind. Fiona is nice. Gary is cold. Gary is kind. Gary is nice. Gary is white. If Fiona is cold then Fiona is furry. If someone is furry then they are red. Blue people are cold. Nice, red people are white. Red people are white. All cold people are furry.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is white.
("Gary" "is" "white" "+")
If Fiona is cold then Fiona is furry.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "furry" "+"))
If someone is furry then they are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
Blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
Nice, red people are white.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
Red people are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
All cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
Bob is white.
True
1
proof
[(triple4 OR ((((((triple2) -> rule6)) -> rule2)) -> rule5) OR ((((((((triple1) -> rule3)) -> rule6)) -> rule2)) -> rule5))]
("Bob" "is" "white" "+")
triple4
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((((((triple1) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
Bob is not kind.
False
1
inv-proof
[(triple3)]
("Bob" "is" "kind" "-")
triple3
Dave is white.
True
2
proof
[(((triple9) -> rule5) OR ((((triple7) -> rule2)) -> rule5) OR ((((((triple6) -> rule6)) -> rule2)) -> rule5) OR ((((((((triple5) -> rule3)) -> rule6)) -> rule2)) -> rule5))]
("Dave" "is" "white" "+")
((triple9) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
((((((((triple5) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Fiona is not furry.
False
2
inv-proof
[(((triple10) -> rule1) OR ((triple10) -> rule6))]
("Fiona" "is" "furry" "-")
((triple10) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple10) -> (rule6 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is red.
True
3
proof
[(((((triple10) -> rule1)) -> rule2) OR ((((triple10) -> rule6)) -> rule2))]
("Fiona" "is" "red" "+")
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((((triple10) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is not red.
False
3
inv-proof
[(((((triple10) -> rule1)) -> rule2) OR ((((triple10) -> rule6)) -> rule2))]
("Fiona" "is" "red" "-")
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((((triple10) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is white.
True
4
proof
[(((((((triple10) -> rule1)) -> rule2)) -> rule5) OR ((((((triple10) -> rule6)) -> rule2)) -> rule5) OR ((triple12 ((((triple10) -> rule1)) -> rule2)) -> rule4) OR ((triple12 ((((triple10) -> rule6)) -> rule2)) -> rule4))]
("Fiona" "is" "white" "+")
((((((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((((((triple10) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((triple12 ((((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((triple12 ((((triple10) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is not white.
False
4
inv-proof
[(((((((triple10) -> rule1)) -> rule2)) -> rule5) OR ((((((triple10) -> rule6)) -> rule2)) -> rule5) OR ((triple12 ((((triple10) -> rule1)) -> rule2)) -> rule4) OR ((triple12 ((((triple10) -> rule6)) -> rule2)) -> rule4))]
("Fiona" "is" "white" "-")
((((((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((((((triple10) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((triple12 ((((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((triple12 ((((triple10) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2 OR ((triple1) -> rule3))] Bob is kind.[(triple3)] Bob is white.[(triple4 OR ((((((triple2) -> rule6)) -> rule2)) -> rule5) OR ((((((((triple1) -> rule3)) -> rule6)) -> rule2)) -> rule5))] Dave is blue.[(triple5)] Dave is cold.[(triple6 OR ((triple5) -> rule3))] Dave is furry.[(triple7 OR ((triple6) -> rule6) OR ((((triple5) -> rule3)) -> rule6))] Dave is kind.[(triple8)] Dave is red.[(triple9 OR ((triple7) -> rule2) OR ((((triple6) -> rule6)) -> rule2) OR ((((((triple5) -> rule3)) -> rule6)) -> rule2))] Fiona is cold.[(triple10)] Fiona is kind.[(triple11)] Fiona is nice.[(triple12)] Gary is cold.[(triple13)] Gary is kind.[(triple14)] Gary is nice.[(triple15)] Gary is white.[(triple16 OR ((((((triple13) -> rule6)) -> rule2)) -> rule5) OR ((triple15 ((((triple13) -> rule6)) -> rule2)) -> rule4))] @1: Bob is furry.[(((triple2) -> rule6) OR ((((triple1) -> rule3)) -> rule6))] Dave is white.[(((triple9) -> rule5) OR ((((triple7) -> rule2)) -> rule5) OR ((((((triple6) -> rule6)) -> rule2)) -> rule5) OR ((((((((triple5) -> rule3)) -> rule6)) -> rule2)) -> rule5))] Fiona is furry.[(((triple10) -> rule1) OR ((triple10) -> rule6))] Gary is furry.[(((triple13) -> rule6))] @2: Bob is red.[(((((triple2) -> rule6)) -> rule2) OR ((((((triple1) -> rule3)) -> rule6)) -> rule2))] Fiona is red.[(((((triple10) -> rule1)) -> rule2) OR ((((triple10) -> rule6)) -> rule2))] Gary is red.[(((((triple13) -> rule6)) -> rule2))] @3: Fiona is white.[(((((((triple10) -> rule1)) -> rule2)) -> rule5) OR ((((((triple10) -> rule6)) -> rule2)) -> rule5) OR ((triple12 ((((triple10) -> rule1)) -> rule2)) -> rule4) OR ((triple12 ((((triple10) -> rule6)) -> rule2)) -> rule4))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((((((triple1) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is cold.
("Dave" "is" "cold" "+")
triple6
((triple5) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple7
((triple6) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Dave is red.
("Dave" "is" "red" "+")
triple9
((triple7) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple10
Fiona is kind.
("Fiona" "is" "kind" "+")
triple11
Fiona is nice.
("Fiona" "is" "nice" "+")
triple12
Gary is cold.
("Gary" "is" "cold" "+")
triple13
Gary is kind.
("Gary" "is" "kind" "+")
triple14
Gary is nice.
("Gary" "is" "nice" "+")
triple15
Gary is white.
("Gary" "is" "white" "+")
triple16
((((((triple13) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((triple15 ((((triple13) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
((triple2) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((triple9) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
((((((((triple5) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple10) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple10) -> (rule6 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple13) -> (rule6 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((((triple10) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((((triple13) -> (rule6 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((((((triple10) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((triple12 ((((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((triple12 ((((triple10) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3