Anne is not nice. Anne is quiet. Charlie is white. Dave is nice. Dave is white. Fiona is furry. Fiona is quiet. All kind people are blue. If someone is kind and nice then they are blue. If Fiona is big and Fiona is not white then Fiona is quiet. If Anne is nice then Anne is white. Kind, blue people are not big. All blue people are nice. White people are kind. Blue, quiet people are furry. If someone is kind and not big then they are quiet.
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
All kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is kind and nice then they are blue.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If Fiona is big and Fiona is not white then Fiona is quiet.
((("Fiona" "is" "big" "+") ("Fiona" "is" "white" "~")) -> ("Fiona" "is" "quiet" "+"))
If Anne is nice then Anne is white.
((("Anne" "is" "nice" "+")) -> ("Anne" "is" "white" "+"))
Kind, blue people are not big.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "-"))
All blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
White people are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
Blue, quiet people are furry.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If someone is kind and not big then they are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "quiet" "+"))
Fiona is quiet.
True
1
proof
[(triple7)]
("Fiona" "is" "quiet" "+")
triple7
Fiona is not furry.
False
1
inv-proof
[(triple6)]
("Fiona" "is" "furry" "-")
triple6
Charlie is kind.
True
2
proof
[(((triple3) -> rule7))]
("Charlie" "is" "kind" "+")
((triple3) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Dave is not kind.
False
2
inv-proof
[(((triple5) -> rule7))]
("Dave" "is" "kind" "-")
((triple5) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
True
3
proof
[(((((triple5) -> rule7)) -> rule1) OR ((((triple5) -> rule7) triple4) -> rule2))]
("Dave" "is" "blue" "+")
((((triple5) -> (rule7 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple5) -> (rule7 % int2)) triple4) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not blue.
False
3
inv-proof
[(((((triple5) -> rule7)) -> rule1) OR ((((triple5) -> rule7) triple4) -> rule2))]
("Dave" "is" "blue" "-")
((((triple5) -> (rule7 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple5) -> (rule7 % int2)) triple4) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Charlie is not big.
True
6
proof
[(((((triple3) -> rule7) ((((triple3) -> rule7)) -> rule1)) -> rule5))]
("Charlie" "is" "big" "-")
((((triple3) -> (rule7 % int3)) ((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is big.
False
6
inv-proof
[(((((triple3) -> rule7) ((((triple3) -> rule7)) -> rule1)) -> rule5))]
("Charlie" "is" "big" "+")
((((triple3) -> (rule7 % int3)) ((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is quiet.
True
9
proof
[(((((triple3) -> rule7) ((((triple3) -> rule7) ((((triple3) -> rule7)) -> rule1)) -> rule5)) -> rule9))]
("Charlie" "is" "quiet" "+")
((((triple3) -> (rule7 % int4)) ((((triple3) -> (rule7 % int4)) ((((triple3) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not big.
("Charlie" "is" "big" "-")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Dave is not quiet.
False
9
inv-proof
[(((((triple5) -> rule7) ((((triple5) -> rule7) ((((triple5) -> rule7)) -> rule1)) -> rule5)) -> rule9) OR ((((triple5) -> rule7) ((((triple5) -> rule7) ((((triple5) -> rule7) triple4) -> rule2)) -> rule5)) -> rule9))]
("Dave" "is" "quiet" "-")
((((triple5) -> (rule7 % int4)) ((((triple5) -> (rule7 % int4)) ((((triple5) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not big.
("Dave" "is" "big" "-")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
((((triple5) -> (rule7 % int4)) ((((triple5) -> (rule7 % int4)) ((((triple5) -> (rule7 % int4)) triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not big.
("Dave" "is" "big" "-")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is furry.
True
13
proof
[(((((((triple5) -> rule7)) -> rule1) ((((triple5) -> rule7) ((((triple5) -> rule7) ((((triple5) -> rule7)) -> rule1)) -> rule5)) -> rule9)) -> rule8) OR ((((((triple5) -> rule7)) -> rule1) ((((triple5) -> rule7) ((((triple5) -> rule7) ((((triple5) -> rule7) triple4) -> rule2)) -> rule5)) -> rule9)) -> rule8) OR ((((((triple5) -> rule7) triple4) -> rule2) ((((triple5) -> rule7) ((((triple5) -> rule7) ((((triple5) -> rule7)) -> rule1)) -> rule5)) -> rule9)) -> rule8) OR ((((((triple5) -> rule7) triple4) -> rule2) ((((triple5) -> rule7) ((((triple5) -> rule7) ((((triple5) -> rule7) triple4) -> rule2)) -> rule5)) -> rule9)) -> rule8))]
("Dave" "is" "furry" "+")
((((((triple5) -> (rule7 % int5))) -> (rule1 % int4)) ((((triple5) -> (rule7 % int5)) ((((triple5) -> (rule7 % int5)) ((((triple5) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not big.
("Dave" "is" "big" "-")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5
((((((triple5) -> (rule7 % int5))) -> (rule1 % int4)) ((((triple5) -> (rule7 % int5)) ((((triple5) -> (rule7 % int5)) ((((triple5) -> (rule7 % int5)) triple4) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not big.
("Dave" "is" "big" "-")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5
((((((triple5) -> (rule7 % int5)) triple4) -> (rule2 % int4)) ((((triple5) -> (rule7 % int5)) ((((triple5) -> (rule7 % int5)) ((((triple5) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not big.
("Dave" "is" "big" "-")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5
((((((triple5) -> (rule7 % int5)) triple4) -> (rule2 % int4)) ((((triple5) -> (rule7 % int5)) ((((triple5) -> (rule7 % int5)) ((((triple5) -> (rule7 % int5)) triple4) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not big.
("Dave" "is" "big" "-")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5
Charlie is not furry.
False
13
inv-proof
[(((((((triple3) -> rule7)) -> rule1) ((((triple3) -> rule7) ((((triple3) -> rule7) ((((triple3) -> rule7)) -> rule1)) -> rule5)) -> rule9)) -> rule8))]
("Charlie" "is" "furry" "-")
((((((triple3) -> (rule7 % int5))) -> (rule1 % int4)) ((((triple3) -> (rule7 % int5)) ((((triple3) -> (rule7 % int5)) ((((triple3) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not big.
("Charlie" "is" "big" "-")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
int5
Anne is not furry.
Unknown
inv-rconc
[@4: Anne is furry.[CWA. Example of deepest failure = (rule8 <- rule1 <- rule7 <- rule4 <- FAIL)]]
("Anne" "is" "furry" "-")
Fiona is blue.
Unknown
rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not nice.
Unknown
inv-rconc
[@3: Fiona is nice.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule7 <- FAIL)]]
("Fiona" "is" "nice" "-")
Anne is white.
Unknown
rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "white" "+")
Anne is not kind.
Unknown
inv-rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("Anne" "is" "kind" "-")
Fiona is kind.
Unknown
rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is not nice.[(triple1)] Anne is quiet.[(triple2)] Charlie is white.[(triple3)] Dave is nice.[(triple4 OR ((((((triple5) -> rule7)) -> rule1)) -> rule6))] Dave is white.[(triple5)] Fiona is furry.[(triple6)] Fiona is quiet.[(triple7)] @1: Charlie is kind.[(((triple3) -> rule7))] Dave is kind.[(((triple5) -> rule7))] @2: Charlie is blue.[(((((triple3) -> rule7)) -> rule1))] Dave is blue.[(((((triple5) -> rule7)) -> rule1) OR ((((triple5) -> rule7) triple4) -> rule2))] @3: Charlie is nice.[(((((((triple3) -> rule7)) -> rule1)) -> rule6))] Charlie is not big.[(((((triple3) -> rule7) ((((triple3) -> rule7)) -> rule1)) -> rule5))] Dave is not big.[(((((triple5) -> rule7) ((((triple5) -> rule7)) -> rule1)) -> rule5) OR ((((triple5) -> rule7) ((((triple5) -> rule7) triple4) -> rule2)) -> rule5))] @4: Charlie is quiet.[(((((triple3) -> rule7) ((((triple3) -> rule7) ((((triple3) -> rule7)) -> rule1)) -> rule5)) -> rule9))] Dave is quiet.[(((((triple5) -> rule7) ((((triple5) -> rule7) ((((triple5) -> rule7)) -> rule1)) -> rule5)) -> rule9) OR ((((triple5) -> rule7) ((((triple5) -> rule7) ((((triple5) -> rule7) triple4) -> rule2)) -> rule5)) -> rule9))] @5: Charlie is furry.[(((((((triple3) -> rule7)) -> rule1) ((((triple3) -> rule7) ((((triple3) -> rule7) ((((triple3) -> rule7)) -> rule1)) -> rule5)) -> rule9)) -> rule8))] Dave is furry.[(((((((triple5) -> rule7)) -> rule1) ((((triple5) -> rule7) ((((triple5) -> rule7) ((((triple5) -> rule7)) -> rule1)) -> rule5)) -> rule9)) -> rule8) OR ((((((triple5) -> rule7)) -> rule1) ((((triple5) -> rule7) ((((triple5) -> rule7) ((((triple5) -> rule7) triple4) -> rule2)) -> rule5)) -> rule9)) -> rule8) OR ((((((triple5) -> rule7) triple4) -> rule2) ((((triple5) -> rule7) ((((triple5) -> rule7) ((((triple5) -> rule7)) -> rule1)) -> rule5)) -> rule9)) -> rule8) OR ((((((triple5) -> rule7) triple4) -> rule2) ((((triple5) -> rule7) ((((triple5) -> rule7) ((((triple5) -> rule7) triple4) -> rule2)) -> rule5)) -> rule9)) -> rule8))]
Anne is not nice.
("Anne" "is" "nice" "-")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
((((((triple5) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
triple5
Fiona is furry.
("Fiona" "is" "furry" "+")
triple6
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple3) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple5) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((((triple5) -> (rule7 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple5) -> (rule7 % int2)) triple4) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not big.
("Charlie" "is" "big" "-")
((((triple3) -> (rule7 % int3)) ((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Dave is not big.
("Dave" "is" "big" "-")
((((triple5) -> (rule7 % int3)) ((((triple5) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((((triple5) -> (rule7 % int3)) ((((triple5) -> (rule7 % int3)) triple4) -> (rule2 % int2))) -> (rule5 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple3) -> (rule7 % int4)) ((((triple3) -> (rule7 % int4)) ((((triple3) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not big.
("Charlie" "is" "big" "-")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple5) -> (rule7 % int4)) ((((triple5) -> (rule7 % int4)) ((((triple5) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not big.
("Dave" "is" "big" "-")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
((((triple5) -> (rule7 % int4)) ((((triple5) -> (rule7 % int4)) ((((triple5) -> (rule7 % int4)) triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not big.
("Dave" "is" "big" "-")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
((((((triple3) -> (rule7 % int5))) -> (rule1 % int4)) ((((triple3) -> (rule7 % int5)) ((((triple3) -> (rule7 % int5)) ((((triple3) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not big.
("Charlie" "is" "big" "-")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
int5
Dave is furry.
("Dave" "is" "furry" "+")
((((((triple5) -> (rule7 % int5))) -> (rule1 % int4)) ((((triple5) -> (rule7 % int5)) ((((triple5) -> (rule7 % int5)) ((((triple5) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not big.
("Dave" "is" "big" "-")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5
((((((triple5) -> (rule7 % int5))) -> (rule1 % int4)) ((((triple5) -> (rule7 % int5)) ((((triple5) -> (rule7 % int5)) ((((triple5) -> (rule7 % int5)) triple4) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not big.
("Dave" "is" "big" "-")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5
((((((triple5) -> (rule7 % int5)) triple4) -> (rule2 % int4)) ((((triple5) -> (rule7 % int5)) ((((triple5) -> (rule7 % int5)) ((((triple5) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not big.
("Dave" "is" "big" "-")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5
((((((triple5) -> (rule7 % int5)) triple4) -> (rule2 % int4)) ((((triple5) -> (rule7 % int5)) ((((triple5) -> (rule7 % int5)) ((((triple5) -> (rule7 % int5)) triple4) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not big.
("Dave" "is" "big" "-")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5