Charlie is blue. Charlie is furry. Charlie is green. Charlie is nice. Charlie is quiet. Charlie is red. Charlie is white. If Charlie is nice and Charlie is white then Charlie is red. Furry people are white. If Charlie is white and Charlie is nice then Charlie is blue. If someone is red then they are nice. If Charlie is red then Charlie is blue. If someone is quiet and blue then they are green. If someone is red and quiet then they are nice. Blue, quiet people are furry.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
If Charlie is nice and Charlie is white then Charlie is red.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "red" "+"))
Furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If Charlie is white and Charlie is nice then Charlie is blue.
((("Charlie" "is" "white" "+") ("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "blue" "+"))
If someone is red then they are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If Charlie is red then Charlie is blue.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "blue" "+"))
If someone is quiet and blue then they are green.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
If someone is red and quiet then they are nice.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Blue, quiet people are furry.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
Charlie is green.
True
1
proof
[(triple3 OR ((triple5 triple1) -> rule6) OR ((triple5 ((triple6) -> rule5)) -> rule6) OR ((triple5 ((triple7 triple4) -> rule3)) -> rule6) OR ((triple5 ((((triple4 triple7) -> rule1)) -> rule5)) -> rule6) OR ((triple5 ((triple7 ((triple6) -> rule4)) -> rule3)) -> rule6) OR ((triple5 ((triple7 ((triple6 triple5) -> rule7)) -> rule3)) -> rule6) OR ((triple5 ((((triple2) -> rule2) triple4) -> rule3)) -> rule6) OR ((triple5 ((((triple2) -> rule2) ((triple6) -> rule4)) -> rule3)) -> rule6) OR ((triple5 ((((triple2) -> rule2) ((triple6 triple5) -> rule7)) -> rule3)) -> rule6) OR ((triple5 ((((triple4 ((triple2) -> rule2)) -> rule1)) -> rule5)) -> rule6))]
("Charlie" "is" "green" "+")
triple3
((triple5 triple1) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple5 ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((triple5 ((triple7 triple4) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((triple5 ((((triple4 triple7) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((triple5 ((triple7 ((triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((triple5 ((triple7 ((triple6 triple5) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((triple5 ((((triple2) -> (rule2 % int3)) triple4) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((triple5 ((((triple2) -> (rule2 % int4)) ((triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
((triple5 ((((triple2) -> (rule2 % int4)) ((triple6 triple5) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
((triple5 ((((triple4 ((triple2) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is not white.
False
1
inv-proof
[(triple7 OR ((triple2) -> rule2) OR ((((triple1 triple5) -> rule8)) -> rule2) OR ((((((triple6) -> rule5) triple5) -> rule8)) -> rule2))]
("Charlie" "is" "white" "-")
triple7
((triple2) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple1 triple5) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((((triple6) -> (rule5 % int3)) triple5) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
@0: Charlie is blue.[(triple1 OR ((triple6) -> rule5) OR ((triple7 triple4) -> rule3) OR ((((triple4 triple7) -> rule1)) -> rule5) OR ((triple7 ((triple6) -> rule4)) -> rule3) OR ((triple7 ((triple6 triple5) -> rule7)) -> rule3) OR ((((triple2) -> rule2) triple4) -> rule3) OR ((((triple2) -> rule2) ((triple6) -> rule4)) -> rule3) OR ((((triple2) -> rule2) ((triple6 triple5) -> rule7)) -> rule3) OR ((((triple4 ((triple2) -> rule2)) -> rule1)) -> rule5))] Charlie is furry.[(triple2 OR ((triple1 triple5) -> rule8) OR ((((triple6) -> rule5) triple5) -> rule8) OR ((((triple7 triple4) -> rule3) triple5) -> rule8) OR ((((((triple4 triple7) -> rule1)) -> rule5) triple5) -> rule8) OR ((((triple7 ((triple6) -> rule4)) -> rule3) triple5) -> rule8) OR ((((triple7 ((triple6 triple5) -> rule7)) -> rule3) triple5) -> rule8))] Charlie is green.[(triple3 OR ((triple5 triple1) -> rule6) OR ((triple5 ((triple6) -> rule5)) -> rule6) OR ((triple5 ((triple7 triple4) -> rule3)) -> rule6) OR ((triple5 ((((triple4 triple7) -> rule1)) -> rule5)) -> rule6) OR ((triple5 ((triple7 ((triple6) -> rule4)) -> rule3)) -> rule6) OR ((triple5 ((triple7 ((triple6 triple5) -> rule7)) -> rule3)) -> rule6) OR ((triple5 ((((triple2) -> rule2) triple4) -> rule3)) -> rule6) OR ((triple5 ((((triple2) -> rule2) ((triple6) -> rule4)) -> rule3)) -> rule6) OR ((triple5 ((((triple2) -> rule2) ((triple6 triple5) -> rule7)) -> rule3)) -> rule6) OR ((triple5 ((((triple4 ((triple2) -> rule2)) -> rule1)) -> rule5)) -> rule6))] Charlie is nice.[(triple4 OR ((triple6) -> rule4) OR ((triple6 triple5) -> rule7))] Charlie is quiet.[(triple5)] Charlie is red.[(triple6 OR ((triple4 triple7) -> rule1) OR ((triple4 ((triple2) -> rule2)) -> rule1) OR ((triple4 ((((triple1 triple5) -> rule8)) -> rule2)) -> rule1))] Charlie is white.[(triple7 OR ((triple2) -> rule2) OR ((((triple1 triple5) -> rule8)) -> rule2) OR ((((((triple6) -> rule5) triple5) -> rule8)) -> rule2))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple6) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple7 triple4) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple4 triple7) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((triple7 ((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((triple7 ((triple6 triple5) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((triple2) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple2) -> (rule2 % int3)) ((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((triple2) -> (rule2 % int3)) ((triple6 triple5) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((triple4 ((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
((triple1 triple5) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple6) -> (rule5 % int2)) triple5) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple7 triple4) -> (rule3 % int2)) triple5) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((((triple4 triple7) -> (rule1 % int3))) -> (rule5 % int2)) triple5) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((((triple7 ((triple6) -> (rule4 % int3))) -> (rule3 % int2)) triple5) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((((triple7 ((triple6 triple5) -> (rule7 % int3))) -> (rule3 % int2)) triple5) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
triple3
((triple5 triple1) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple5 ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((triple5 ((triple7 triple4) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((triple5 ((((triple4 triple7) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((triple5 ((triple7 ((triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((triple5 ((triple7 ((triple6 triple5) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((triple5 ((((triple2) -> (rule2 % int3)) triple4) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((triple5 ((((triple2) -> (rule2 % int4)) ((triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
((triple5 ((((triple2) -> (rule2 % int4)) ((triple6 triple5) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
((triple5 ((((triple4 ((triple2) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
((triple6) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple6 triple5) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
((triple4 triple7) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple4 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((triple4 ((((triple1 triple5) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
triple7
((triple2) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple1 triple5) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((((triple6) -> (rule5 % int3)) triple5) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3