Bob is cold. Dave is blue. Dave is cold. Dave is furry. Dave is quiet. Dave is white. Erin is furry. Erin is red. Fiona is cold. Fiona is furry. If something is red and cold then it is quiet. If something is big then it is blue. All blue, big things are white. If Erin is quiet then Erin is furry. If Fiona is not furry then Fiona is quiet. If Fiona is blue and Fiona is white then Fiona is quiet. If Bob is furry and Bob is cold then Bob is white. Quiet things are big. If something is furry then it is red.
Bob is cold.
("Bob" "is" "cold" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
If something is red and cold then it is quiet.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
If something is big then it is blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
All blue, big things are white.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If Erin is quiet then Erin is furry.
((("Erin" "is" "quiet" "+")) -> ("Erin" "is" "furry" "+"))
If Fiona is not furry then Fiona is quiet.
((("Fiona" "is" "furry" "~")) -> ("Fiona" "is" "quiet" "+"))
If Fiona is blue and Fiona is white then Fiona is quiet.
((("Fiona" "is" "blue" "+") ("Fiona" "is" "white" "+")) -> ("Fiona" "is" "quiet" "+"))
If Bob is furry and Bob is cold then Bob is white.
((("Bob" "is" "furry" "+") ("Bob" "is" "cold" "+")) -> ("Bob" "is" "white" "+"))
Quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If something is furry then it is red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
Dave is cold.
True
1
proof
[(triple3)]
("Dave" "is" "cold" "+")
triple3
Erin is not red.
False
1
inv-proof
[(triple8 OR ((triple7) -> rule9))]
("Erin" "is" "red" "-")
triple8
((triple7) -> (rule9 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Dave is big.
True
2
proof
[(((triple5) -> rule8) OR ((((((triple4) -> rule9) triple3) -> rule1)) -> rule8))]
("Dave" "is" "big" "+")
((triple5) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((((triple4) -> (rule9 % int3)) triple3) -> (rule1 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is not big.
False
2
inv-proof
[(((triple5) -> rule8) OR ((((((triple4) -> rule9) triple3) -> rule1)) -> rule8))]
("Dave" "is" "big" "-")
((triple5) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((((triple4) -> (rule9 % int3)) triple3) -> (rule1 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Fiona is quiet.
True
4
proof
[(((((triple10) -> rule9) triple9) -> rule1))]
("Fiona" "is" "quiet" "+")
((((triple10) -> (rule9 % int2)) triple9) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is not quiet.
False
4
inv-proof
[(((((triple10) -> rule9) triple9) -> rule1))]
("Fiona" "is" "quiet" "-")
((((triple10) -> (rule9 % int2)) triple9) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is big.
True
5
proof
[(((((((triple10) -> rule9) triple9) -> rule1)) -> rule8))]
("Fiona" "is" "big" "+")
((((((triple10) -> (rule9 % int3)) triple9) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is not big.
False
5
inv-proof
[(((((((triple10) -> rule9) triple9) -> rule1)) -> rule8))]
("Fiona" "is" "big" "-")
((((((triple10) -> (rule9 % int3)) triple9) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is blue.
True
6
proof
[(((((((((triple10) -> rule9) triple9) -> rule1)) -> rule8)) -> rule2))]
("Fiona" "is" "blue" "+")
((((((((triple10) -> (rule9 % int4)) triple9) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is not blue.
False
6
inv-proof
[(((((((((triple10) -> rule9) triple9) -> rule1)) -> rule8)) -> rule2))]
("Fiona" "is" "blue" "-")
((((((((triple10) -> (rule9 % int4)) triple9) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is white.
True
12
proof
[(((((((((((triple10) -> rule9) triple9) -> rule1)) -> rule8)) -> rule2) ((((((triple10) -> rule9) triple9) -> rule1)) -> rule8)) -> rule3))]
("Fiona" "is" "white" "+")
((((((((((triple10) -> (rule9 % int5)) triple9) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule2 % int2)) ((((((triple10) -> (rule9 % int5)) triple9) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is red.
("Fiona" "is" "red" "+")
int5
Fiona is not white.
False
12
inv-proof
[(((((((((((triple10) -> rule9) triple9) -> rule1)) -> rule8)) -> rule2) ((((((triple10) -> rule9) triple9) -> rule1)) -> rule8)) -> rule3))]
("Fiona" "is" "white" "-")
((((((((((triple10) -> (rule9 % int5)) triple9) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule2 % int2)) ((((((triple10) -> (rule9 % int5)) triple9) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is red.
("Fiona" "is" "red" "+")
int5
Erin is not blue.
Unknown
inv-rconc
[@3: Erin is blue.[CWA. Example of deepest failure = (rule2 <- rule8 <- rule1 <- FAIL)]]
("Erin" "is" "blue" "-")
Bob is quiet.
Unknown
rconc
[@2: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- rule9 <- FAIL)]]
("Bob" "is" "quiet" "+")
Erin is not white.
Unknown
inv-rconc
[@3: Erin is white.[CWA. Example of deepest failure = (rule3 <- rule8 <- rule1 <- FAIL)]]
("Erin" "is" "white" "-")
Bob is blue.
Unknown
rconc
[@4: Bob is blue.[CWA. Example of deepest failure = (rule2 <- rule8 <- rule1 <- rule9 <- FAIL)]]
("Bob" "is" "blue" "+")
Bob is not big.
Unknown
inv-rconc
[@3: Bob is big.[CWA. Example of deepest failure = (rule8 <- rule1 <- rule9 <- FAIL)]]
("Bob" "is" "big" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is cold.[(triple1)] Dave is blue.[(triple2 OR ((((triple5) -> rule8)) -> rule2) OR ((((((((triple4) -> rule9) triple3) -> rule1)) -> rule8)) -> rule2))] Dave is cold.[(triple3)] Dave is furry.[(triple4)] Dave is quiet.[(triple5 OR ((((triple4) -> rule9) triple3) -> rule1))] Dave is white.[(triple6 OR ((triple2 ((triple5) -> rule8)) -> rule3) OR ((((((triple5) -> rule8)) -> rule2) ((triple5) -> rule8)) -> rule3) OR ((triple2 ((((((triple4) -> rule9) triple3) -> rule1)) -> rule8)) -> rule3) OR ((((((triple5) -> rule8)) -> rule2) ((((((triple4) -> rule9) triple3) -> rule1)) -> rule8)) -> rule3) OR ((((((((((triple4) -> rule9) triple3) -> rule1)) -> rule8)) -> rule2) ((triple5) -> rule8)) -> rule3) OR ((((((((((triple4) -> rule9) triple3) -> rule1)) -> rule8)) -> rule2) ((((((triple4) -> rule9) triple3) -> rule1)) -> rule8)) -> rule3))] Erin is furry.[(triple7)] Erin is red.[(triple8 OR ((triple7) -> rule9))] Fiona is cold.[(triple9)] Fiona is furry.[(triple10)] @1: Dave is big.[(((triple5) -> rule8) OR ((((((triple4) -> rule9) triple3) -> rule1)) -> rule8))] Dave is red.[(((triple4) -> rule9))] Fiona is red.[(((triple10) -> rule9))] @2: Fiona is quiet.[(((((triple10) -> rule9) triple9) -> rule1))] @3: Fiona is big.[(((((((triple10) -> rule9) triple9) -> rule1)) -> rule8))] @4: Fiona is blue.[(((((((((triple10) -> rule9) triple9) -> rule1)) -> rule8)) -> rule2))] @5: Fiona is white.[(((((((((((triple10) -> rule9) triple9) -> rule1)) -> rule8)) -> rule2) ((((((triple10) -> rule9) triple9) -> rule1)) -> rule8)) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
((((triple5) -> (rule8 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((((((triple4) -> (rule9 % int4)) triple3) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
((((triple4) -> (rule9 % int2)) triple3) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
triple6
((triple2 ((triple5) -> (rule8 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((((triple5) -> (rule8 % int3))) -> (rule2 % int2)) ((triple5) -> (rule8 % int3))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((triple2 ((((((triple4) -> (rule9 % int4)) triple3) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
((((((triple5) -> (rule8 % int5))) -> (rule2 % int4)) ((((((triple4) -> (rule9 % int3)) triple3) -> (rule1 % int2))) -> (rule8 % int5))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is big.
("Dave" "is" "big" "+")
int5
((((((((((triple4) -> (rule9 % int5)) triple3) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule2 % int2)) ((triple5) -> (rule8 % int3))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
int5
((((((((((triple4) -> (rule9 % int5)) triple3) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule2 % int2)) ((((((triple4) -> (rule9 % int5)) triple3) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
int5
Erin is furry.
("Erin" "is" "furry" "+")
triple7
Erin is red.
("Erin" "is" "red" "+")
triple8
((triple7) -> (rule9 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple9
Fiona is furry.
("Fiona" "is" "furry" "+")
triple10
Dave is big.
("Dave" "is" "big" "+")
((triple5) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((((triple4) -> (rule9 % int3)) triple3) -> (rule1 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((triple4) -> (rule9 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple10) -> (rule9 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple10) -> (rule9 % int2)) triple9) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
((((((triple10) -> (rule9 % int3)) triple9) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
((((((((triple10) -> (rule9 % int4)) triple9) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
((((((((((triple10) -> (rule9 % int5)) triple9) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule2 % int2)) ((((((triple10) -> (rule9 % int5)) triple9) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is red.
("Fiona" "is" "red" "+")
int5