Bob is white. Charlie is blue. Charlie is white. Erin is green. Fiona is quiet. Fiona is red. Fiona is white. Quiet things are blue. All smart, big things are green. All white, quiet things are blue. If something is white and red then it is big. Quiet, green things are big. Green, blue things are red. All green things are white. If something is red and big then it is smart. All white things are blue.
Bob is white.
("Bob" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is green.
("Erin" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
All smart, big things are green.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
All white, quiet things are blue.
((("something" "is" "white" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If something is white and red then it is big.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Quiet, green things are big.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
Green, blue things are red.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
All green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is red and big then it is smart.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
All white things are blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
Bob is white.
True
1
proof
[(triple1)]
("Bob" "is" "white" "+")
triple1
Charlie is not blue.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule9))]
("Charlie" "is" "blue" "-")
triple2
((triple3) -> (rule9 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Fiona is blue.
True
2
proof
[(((triple5) -> rule1) OR ((triple7) -> rule9) OR ((triple7 triple5) -> rule3))]
("Fiona" "is" "blue" "+")
((triple5) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple7) -> (rule9 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple7 triple5) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is not blue.
False
2
inv-proof
[(((triple5) -> rule1) OR ((triple7) -> rule9) OR ((triple7 triple5) -> rule3))]
("Fiona" "is" "blue" "-")
((triple5) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple7) -> (rule9 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple7 triple5) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
True
5
proof
[(((triple6 ((triple7 triple6) -> rule4)) -> rule8))]
("Fiona" "is" "smart" "+")
((triple6 ((triple7 triple6) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Erin is not blue.
False
3
inv-proof
[(((((triple4) -> rule7)) -> rule9))]
("Erin" "is" "blue" "-")
((((triple4) -> (rule7 % int2))) -> (rule9 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Fiona is green.
True
9
proof
[(((((triple6 ((triple7 triple6) -> rule4)) -> rule8) ((triple7 triple6) -> rule4)) -> rule2))]
("Fiona" "is" "green" "+")
((((triple6 ((triple7 triple6) -> (rule4 % int3))) -> (rule8 % int2)) ((triple7 triple6) -> (rule4 % int3))) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is not green.
False
9
inv-proof
[(((((triple6 ((triple7 triple6) -> rule4)) -> rule8) ((triple7 triple6) -> rule4)) -> rule2))]
("Fiona" "is" "green" "-")
((((triple6 ((triple7 triple6) -> (rule4 % int3))) -> (rule8 % int2)) ((triple7 triple6) -> (rule4 % int3))) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Erin is big.
True
8
proof
[(((((triple4) -> rule7) ((triple4 ((((triple4) -> rule7)) -> rule9)) -> rule6)) -> rule4))]
("Erin" "is" "big" "+")
((((triple4) -> (rule7 % int4)) ((triple4 ((((triple4) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is not big.
False
8
inv-proof
[(((((triple4) -> rule7) ((triple4 ((((triple4) -> rule7)) -> rule9)) -> rule6)) -> rule4))]
("Erin" "is" "big" "-")
((((triple4) -> (rule7 % int4)) ((triple4 ((((triple4) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is smart.
True
14
proof
[(((((triple4 ((((triple4) -> rule7)) -> rule9)) -> rule6) ((((triple4) -> rule7) ((triple4 ((((triple4) -> rule7)) -> rule9)) -> rule6)) -> rule4)) -> rule8))]
("Erin" "is" "smart" "+")
((((triple4 ((((triple4) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule6 % int3)) ((((triple4) -> (rule7 % int5)) ((triple4 ((((triple4) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5
Erin is not smart.
False
14
inv-proof
[(((((triple4 ((((triple4) -> rule7)) -> rule9)) -> rule6) ((((triple4) -> rule7) ((triple4 ((((triple4) -> rule7)) -> rule9)) -> rule6)) -> rule4)) -> rule8))]
("Erin" "is" "smart" "-")
((((triple4 ((((triple4) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule6 % int3)) ((((triple4) -> (rule7 % int5)) ((triple4 ((((triple4) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5
Charlie is not smart.
Unknown
inv-rconc
[@3: Charlie is smart.[CWA. Example of deepest failure = (rule8 <- rule6 <- rule2 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is red.
Unknown
rconc
[@3: Charlie is red.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule8 <- FAIL)]]
("Charlie" "is" "red" "+")
Bob is not smart.
Unknown
inv-rconc
[@3: Bob is smart.[CWA. Example of deepest failure = (rule8 <- rule6 <- rule2 <- FAIL)]]
("Bob" "is" "smart" "-")
Charlie is green.
Unknown
rconc
[@3: Charlie is green.[CWA. Example of deepest failure = (rule2 <- rule8 <- rule6 <- FAIL)]]
("Charlie" "is" "green" "+")
Bob is not big.
Unknown
inv-rconc
[@4: Bob is big.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule2 <- rule8 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is green.
Unknown
rconc
[@3: Bob is green.[CWA. Example of deepest failure = (rule2 <- rule8 <- rule6 <- FAIL)]]
("Bob" "is" "green" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is white.[(triple1)] Charlie is blue.[(triple2 OR ((triple3) -> rule9))] Charlie is white.[(triple3)] Erin is green.[(triple4)] Fiona is quiet.[(triple5)] Fiona is red.[(triple6)] Fiona is white.[(triple7)] @1: Bob is blue.[(((triple1) -> rule9))] Erin is white.[(((triple4) -> rule7))] Fiona is big.[(((triple7 triple6) -> rule4))] Fiona is blue.[(((triple5) -> rule1) OR ((triple7) -> rule9) OR ((triple7 triple5) -> rule3))] @2: Erin is blue.[(((((triple4) -> rule7)) -> rule9))] Fiona is smart.[(((triple6 ((triple7 triple6) -> rule4)) -> rule8))] @3: Erin is red.[(((triple4 ((((triple4) -> rule7)) -> rule9)) -> rule6))] Fiona is green.[(((((triple6 ((triple7 triple6) -> rule4)) -> rule8) ((triple7 triple6) -> rule4)) -> rule2))] @4: Erin is big.[(((((triple4) -> rule7) ((triple4 ((((triple4) -> rule7)) -> rule9)) -> rule6)) -> rule4))] @5: Erin is smart.[(((((triple4 ((((triple4) -> rule7)) -> rule9)) -> rule6) ((((triple4) -> rule7) ((triple4 ((((triple4) -> rule7)) -> rule9)) -> rule6)) -> rule4)) -> rule8))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
((triple3) -> (rule9 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
triple4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple5
Fiona is red.
("Fiona" "is" "red" "+")
triple6
Fiona is white.
("Fiona" "is" "white" "+")
triple7
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule9 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple4) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple7 triple6) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple5) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple7) -> (rule9 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple7 triple5) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((((triple4) -> (rule7 % int2))) -> (rule9 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple6 ((triple7 triple6) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((triple4 ((((triple4) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
((((triple6 ((triple7 triple6) -> (rule4 % int3))) -> (rule8 % int2)) ((triple7 triple6) -> (rule4 % int3))) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
((((triple4) -> (rule7 % int4)) ((triple4 ((((triple4) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
((((triple4 ((((triple4) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule6 % int3)) ((((triple4) -> (rule7 % int5)) ((triple4 ((((triple4) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5