Anne is kind. Anne is red. Anne is smart. Bob is not kind. Bob is nice. Bob is quiet. Charlie is furry. Charlie is quiet. Gary is kind. Gary is quiet. Gary is red. If someone is smart then they are kind. Furry people are kind. All smart people are nice. If someone is furry and nice then they are smart. If someone is blue and kind then they are smart. All furry, red people are blue. If someone is nice and quiet then they are blue. Kind people are red. If Bob is kind then Bob is not nice.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is not kind.
("Bob" "is" "kind" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
If someone is smart then they are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
Furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
All smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If someone is furry and nice then they are smart.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If someone is blue and kind then they are smart.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
All furry, red people are blue.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is nice and quiet then they are blue.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
Kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If Bob is kind then Bob is not nice.
((("Bob" "is" "kind" "+")) -> ("Bob" "is" "nice" "-"))
Bob is quiet.
True
1
proof
[(triple6)]
("Bob" "is" "quiet" "+")
triple6
Bob is not quiet.
False
1
inv-proof
[(triple6)]
("Bob" "is" "quiet" "-")
triple6
Anne is nice.
True
2
proof
[(((triple3) -> rule3))]
("Anne" "is" "nice" "+")
((triple3) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Bob is not blue.
False
3
inv-proof
[(((triple5 triple6) -> rule7))]
("Bob" "is" "blue" "-")
((triple5 triple6) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Charlie is red.
True
3
proof
[(((((triple7) -> rule2)) -> rule8))]
("Charlie" "is" "red" "+")
((((triple7) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not red.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule8))]
("Charlie" "is" "red" "-")
((((triple7) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is blue.
True
5
proof
[(((triple7 ((((triple7) -> rule2)) -> rule8)) -> rule6))]
("Charlie" "is" "blue" "+")
((triple7 ((((triple7) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not blue.
False
5
inv-proof
[(((triple7 ((((triple7) -> rule2)) -> rule8)) -> rule6))]
("Charlie" "is" "blue" "-")
((triple7 ((((triple7) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is smart.
True
8
proof
[(((((triple7 ((((triple7) -> rule2)) -> rule8)) -> rule6) ((triple7) -> rule2)) -> rule5))]
("Charlie" "is" "smart" "+")
((((triple7 ((((triple7) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) ((triple7) -> (rule2 % int4))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is not smart.
False
8
inv-proof
[(((((triple7 ((((triple7) -> rule2)) -> rule8)) -> rule6) ((triple7) -> rule2)) -> rule5))]
("Charlie" "is" "smart" "-")
((((triple7 ((((triple7) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) ((triple7) -> (rule2 % int4))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is nice.
True
9
proof
[(((((((triple7 ((((triple7) -> rule2)) -> rule8)) -> rule6) ((triple7) -> rule2)) -> rule5)) -> rule3))]
("Charlie" "is" "nice" "+")
((((((triple7 ((((triple7) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule6 % int3)) ((triple7) -> (rule2 % int5))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
int5
Charlie is not nice.
False
9
inv-proof
[(((((((triple7 ((((triple7) -> rule2)) -> rule8)) -> rule6) ((triple7) -> rule2)) -> rule5)) -> rule3))]
("Charlie" "is" "nice" "-")
((((((triple7 ((((triple7) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule6 % int3)) ((triple7) -> (rule2 % int5))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
int5
Gary is not smart.
Unknown
inv-rconc
[@4: Gary is smart.[CWA. Example of deepest failure = (rule5 <- rule7 <- rule3 <- rule4 <- FAIL)]]
("Gary" "is" "smart" "-")
Anne is blue.
Unknown
rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "blue" "+")
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "smart" "-")
Gary is nice.
Unknown
rconc
[@3: Gary is nice.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule6 <- FAIL)]]
("Gary" "is" "nice" "+")
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "red" "-")
Gary is blue.
Unknown
rconc
[@4: Gary is blue.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule5 <- rule6 <- FAIL)]]
("Gary" "is" "blue" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is kind.[(triple1 OR ((triple3) -> rule1))] Anne is red.[(triple2 OR ((triple1) -> rule8) OR ((((triple3) -> rule1)) -> rule8))] Anne is smart.[(triple3)] Bob is nice.[(triple5)] Bob is not kind.[(triple4)] Bob is quiet.[(triple6)] Charlie is furry.[(triple7)] Charlie is quiet.[(triple8)] Gary is kind.[(triple9)] Gary is quiet.[(triple10)] Gary is red.[(triple11 OR ((triple9) -> rule8))] @1: Anne is nice.[(((triple3) -> rule3))] Bob is blue.[(((triple5 triple6) -> rule7))] Charlie is kind.[(((triple7) -> rule2))] @2: Charlie is red.[(((((triple7) -> rule2)) -> rule8))] @3: Charlie is blue.[(((triple7 ((((triple7) -> rule2)) -> rule8)) -> rule6))] @4: Charlie is smart.[(((((triple7 ((((triple7) -> rule2)) -> rule8)) -> rule6) ((triple7) -> rule2)) -> rule5))] @5: Charlie is nice.[(((((((triple7 ((((triple7) -> rule2)) -> rule8)) -> rule6) ((triple7) -> rule2)) -> rule5)) -> rule3))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
((triple3) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple2
((triple1) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple5
Bob is not kind.
("Bob" "is" "kind" "-")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple6
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
((triple9) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((triple3) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple5 triple6) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple7) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple7) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple7 ((((triple7) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple7 ((((triple7) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) ((triple7) -> (rule2 % int4))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
((((((triple7 ((((triple7) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule6 % int3)) ((triple7) -> (rule2 % int5))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
int5