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