Anne is red. Anne is smart. Anne is white. Bob is blue. Bob is green. Bob is quiet. Bob is red. Bob is white. Bob is young. Gary is blue. Gary is green. Gary is quiet. Gary is red. Gary is smart. Gary is white. Gary is young. All white people are quiet. If Bob is green and Bob is smart then Bob is blue. All smart, young people are red. If someone is blue then they are smart. If Gary is blue and Gary is smart then Gary is red. If Anne is white then Anne is blue. If Anne is smart and Anne is blue then Anne is green. Red people are blue.
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
All white people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is green and Bob is smart then Bob is blue.
((("Bob" "is" "green" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "blue" "+"))
All smart, young people are red.
((("someone" "is" "smart" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If someone is blue then they are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
If Gary is blue and Gary is smart then Gary is red.
((("Gary" "is" "blue" "+") ("Gary" "is" "smart" "+")) -> ("Gary" "is" "red" "+"))
If Anne is white then Anne is blue.
((("Anne" "is" "white" "+")) -> ("Anne" "is" "blue" "+"))
If Anne is smart and Anne is blue then Anne is green.
((("Anne" "is" "smart" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "green" "+"))
Red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
Bob is blue.
True
1
proof
[(triple4 OR ((triple7) -> rule8))]
("Bob" "is" "blue" "+")
triple4
((triple7) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Gary is not quiet.
False
1
inv-proof
[(triple12 OR ((triple15) -> rule1))]
("Gary" "is" "quiet" "-")
triple12
((triple15) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Anne is quiet.
True
2
proof
[(((triple3) -> rule1))]
("Anne" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not blue.
False
2
inv-proof
[(((triple1) -> rule8) OR ((triple3) -> rule6))]
("Anne" "is" "blue" "-")
((triple1) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple3) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
@0: Anne is red.[(triple1)] Anne is smart.[(triple2 OR ((((triple1) -> rule8)) -> rule4) OR ((((triple3) -> rule6)) -> rule4))] Anne is white.[(triple3)] Bob is blue.[(triple4 OR ((triple7) -> rule8))] Bob is green.[(triple5)] Bob is quiet.[(triple6 OR ((triple8) -> rule1))] Bob is red.[(triple7 OR ((((triple4) -> rule4) triple9) -> rule3))] Bob is white.[(triple8)] Bob is young.[(triple9)] Gary is blue.[(triple10 OR ((triple13) -> rule8) OR ((((triple14 triple16) -> rule3)) -> rule8))] Gary is green.[(triple11)] Gary is quiet.[(triple12 OR ((triple15) -> rule1))] Gary is red.[(triple13 OR ((triple10 triple14) -> rule5) OR ((triple14 triple16) -> rule3) OR ((triple10 ((triple10) -> rule4)) -> rule5) OR ((((triple10) -> rule4) triple16) -> rule3))] Gary is smart.[(triple14 OR ((triple10) -> rule4) OR ((((triple13) -> rule8)) -> rule4))] Gary is white.[(triple15)] Gary is young.[(triple16)] @1: Anne is blue.[(((triple1) -> rule8) OR ((triple3) -> rule6))] Anne is quiet.[(((triple3) -> rule1))] Bob is smart.[(((triple4) -> rule4) OR ((((triple7) -> rule8)) -> rule4))] @2: Anne is green.[(((triple2 ((triple1) -> rule8)) -> rule7) OR ((triple2 ((triple3) -> rule6)) -> rule7) OR ((((((triple1) -> rule8)) -> rule4) ((triple1) -> rule8)) -> rule7) OR ((((((triple1) -> rule8)) -> rule4) ((triple3) -> rule6)) -> rule7) OR ((((((triple3) -> rule6)) -> rule4) ((triple1) -> rule8)) -> rule7) OR ((((((triple3) -> rule6)) -> rule4) ((triple3) -> rule6)) -> rule7))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
triple4
((triple7) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple5
Bob is quiet.
("Bob" "is" "quiet" "+")
triple6
((triple8) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple7
((((triple4) -> (rule4 % int2)) triple9) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
triple8
Bob is young.
("Bob" "is" "young" "+")
triple9
Gary is blue.
("Gary" "is" "blue" "+")
triple10
((triple13) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple14 triple16) -> (rule3 % int2))) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple11
Gary is quiet.
("Gary" "is" "quiet" "+")
triple12
((triple15) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple13
((triple10 triple14) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple14 triple16) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple10 ((triple10) -> (rule4 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple10) -> (rule4 % int2)) triple16) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple14
((triple10) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple13) -> (rule8 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
triple15
Gary is young.
("Gary" "is" "young" "+")
triple16
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple3) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple4) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple7) -> (rule8 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((triple2 ((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((triple2 ((triple3) -> (rule6 % int2))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2)) ((triple1) -> (rule8 % int3))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2)) ((triple3) -> (rule6 % int3))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((((triple3) -> (rule6 % int3))) -> (rule4 % int2)) ((triple1) -> (rule8 % int3))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((((triple3) -> (rule6 % int3))) -> (rule4 % int2)) ((triple3) -> (rule6 % int3))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3