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