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