Anne is blue. Anne is furry. Anne is smart. Bob is blue. Bob is furry. Bob is quiet. Bob is red. Bob is smart. Bob is white. Bob is young. All red, quiet people are smart. All blue, young people are white. If Anne is red and Anne is white then Anne is quiet. Young, smart people are red. Furry people are quiet. All quiet, smart people are young.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
All red, quiet people are smart.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
All blue, young people are white.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If Anne is red and Anne is white then Anne is quiet.
((("Anne" "is" "red" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "quiet" "+"))
Young, smart people are red.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
Furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
All quiet, smart people are young.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
Bob is white.
True
1
proof
[(triple9 OR ((triple4 triple10) -> rule2) OR ((triple4 ((triple6 triple8) -> rule6)) -> rule2) OR ((triple4 ((triple6 ((triple7 triple6) -> rule1)) -> rule6)) -> rule2) OR ((triple4 ((((triple5) -> rule5) triple8) -> rule6)) -> rule2) OR ((triple4 ((((triple5) -> rule5) ((triple7 triple6) -> rule1)) -> rule6)) -> rule2) OR ((triple4 ((triple6 ((triple7 ((triple5) -> rule5)) -> rule1)) -> rule6)) -> rule2) OR ((triple4 ((((triple5) -> rule5) ((triple7 ((triple5) -> rule5)) -> rule1)) -> rule6)) -> rule2))]
("Bob" "is" "white" "+")
triple9
((triple4 triple10) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple4 ((triple6 triple8) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((triple4 ((triple6 ((triple7 triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((triple4 ((((triple5) -> (rule5 % int3)) triple8) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((triple4 ((((triple5) -> (rule5 % int4)) ((triple7 triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
((triple4 ((triple6 ((triple7 ((triple5) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
((triple4 ((((triple5) -> (rule5 % int4)) ((triple7 ((triple5) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is not quiet.
False
1
inv-proof
[(triple6 OR ((triple5) -> rule5))]
("Bob" "is" "quiet" "-")
triple6
((triple5) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Anne is quiet.
True
2
proof
[(((triple2) -> rule5))]
("Anne" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple2) -> rule5))]
("Anne" "is" "quiet" "-")
((triple2) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
True
4
proof
[(((((triple2) -> rule5) triple3) -> rule6))]
("Anne" "is" "young" "+")
((((triple2) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not young.
False
4
inv-proof
[(((((triple2) -> rule5) triple3) -> rule6))]
("Anne" "is" "young" "-")
((((triple2) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is red.
True
6
proof
[(((((((triple2) -> rule5) triple3) -> rule6) triple3) -> rule4))]
("Anne" "is" "red" "+")
((((((triple2) -> (rule5 % int3)) triple3) -> (rule6 % int2)) triple3) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is not white.
False
6
inv-proof
[(((triple1 ((((triple2) -> rule5) triple3) -> rule6)) -> rule2))]
("Anne" "is" "white" "-")
((triple1 ((((triple2) -> (rule5 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2)] Anne is smart.[(triple3)] Bob is blue.[(triple4)] Bob is furry.[(triple5)] Bob is quiet.[(triple6 OR ((triple5) -> rule5))] Bob is red.[(triple7 OR ((triple10 triple8) -> rule4) OR ((((triple6 triple8) -> rule6) triple8) -> rule4) OR ((((((triple5) -> rule5) triple8) -> rule6) triple8) -> rule4))] Bob is smart.[(triple8 OR ((triple7 triple6) -> rule1) OR ((triple7 ((triple5) -> rule5)) -> rule1))] Bob is white.[(triple9 OR ((triple4 triple10) -> rule2) OR ((triple4 ((triple6 triple8) -> rule6)) -> rule2) OR ((triple4 ((triple6 ((triple7 triple6) -> rule1)) -> rule6)) -> rule2) OR ((triple4 ((((triple5) -> rule5) triple8) -> rule6)) -> rule2) OR ((triple4 ((((triple5) -> rule5) ((triple7 triple6) -> rule1)) -> rule6)) -> rule2) OR ((triple4 ((triple6 ((triple7 ((triple5) -> rule5)) -> rule1)) -> rule6)) -> rule2) OR ((triple4 ((((triple5) -> rule5) ((triple7 ((triple5) -> rule5)) -> rule1)) -> rule6)) -> rule2))] Bob is young.[(triple10 OR ((triple6 triple8) -> rule6) OR ((triple6 ((triple7 triple6) -> rule1)) -> rule6) OR ((((triple5) -> rule5) triple8) -> rule6) OR ((((triple5) -> rule5) ((triple7 triple6) -> rule1)) -> rule6) OR ((triple6 ((triple7 ((triple5) -> rule5)) -> rule1)) -> rule6) OR ((((triple5) -> rule5) ((triple7 ((triple5) -> rule5)) -> rule1)) -> rule6))] @1: Anne is quiet.[(((triple2) -> rule5))] @2: Anne is young.[(((((triple2) -> rule5) triple3) -> rule6))] @3: Anne is red.[(((((((triple2) -> rule5) triple3) -> rule6) triple3) -> rule4))] Anne is white.[(((triple1 ((((triple2) -> rule5) triple3) -> rule6)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
triple4
Bob is furry.
("Bob" "is" "furry" "+")
triple5
Bob is quiet.
("Bob" "is" "quiet" "+")
triple6
((triple5) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple7
((triple10 triple8) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple6 triple8) -> (rule6 % int2)) triple8) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((((triple5) -> (rule5 % int3)) triple8) -> (rule6 % int2)) triple8) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
triple8
((triple7 triple6) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple7 ((triple5) -> (rule5 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
triple9
((triple4 triple10) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple4 ((triple6 triple8) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((triple4 ((triple6 ((triple7 triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((triple4 ((((triple5) -> (rule5 % int3)) triple8) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((triple4 ((((triple5) -> (rule5 % int4)) ((triple7 triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
((triple4 ((triple6 ((triple7 ((triple5) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
((triple4 ((((triple5) -> (rule5 % int4)) ((triple7 ((triple5) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is young.
("Bob" "is" "young" "+")
triple10
((triple6 triple8) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple6 ((triple7 triple6) -> (rule1 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple5) -> (rule5 % int2)) triple8) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple5) -> (rule5 % int3)) ((triple7 triple6) -> (rule1 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((triple6 ((triple7 ((triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((triple5) -> (rule5 % int3)) ((triple7 ((triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple2) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((((triple2) -> (rule5 % int3)) triple3) -> (rule6 % int2)) triple3) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
((triple1 ((((triple2) -> (rule5 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3