Anne is big. Anne is round. Anne is white. Dave is big. Dave is kind. Dave is quiet. Dave is red. Dave is round. Dave is white. Gary is big. Gary is kind. Gary is not quiet. Gary is red. Gary is round. Gary is not white. Big people are red. If someone is green then they are red. Round, kind people are big. If someone is big then they are green. All green people are kind. If someone is kind and white then they are quiet. If Gary is quiet and Gary is big then Gary is red. If someone is red and not big then they are white.
Anne is big.
("Anne" "is" "big" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is not white.
("Gary" "is" "white" "-")
Big people are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone is green then they are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Round, kind people are big.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
All green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind and white then they are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is quiet and Gary is big then Gary is red.
((("Gary" "is" "quiet" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "red" "+"))
If someone is red and not big then they are white.
((("someone" "is" "red" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "white" "+"))
Dave is round.
True
1
proof
[(triple8)]
("Dave" "is" "round" "+")
triple8
Gary is not round.
False
1
inv-proof
[(triple14)]
("Gary" "is" "round" "-")
triple14
Dave is green.
True
2
proof
[(((triple4) -> rule4) OR ((((triple8 triple5) -> rule3)) -> rule4))]
("Dave" "is" "green" "+")
((triple4) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple8 triple5) -> (rule3 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not green.
False
2
inv-proof
[(((triple4) -> rule4) OR ((((triple8 triple5) -> rule3)) -> rule4))]
("Dave" "is" "green" "-")
((triple4) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple8 triple5) -> (rule3 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Anne is kind.
True
3
proof
[(((((triple1) -> rule4)) -> rule5))]
("Anne" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not kind.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule5))]
("Anne" "is" "kind" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
True
5
proof
[(((((((triple1) -> rule4)) -> rule5) triple3) -> rule6))]
("Anne" "is" "quiet" "+")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not quiet.
False
5
inv-proof
[(((((((triple1) -> rule4)) -> rule5) triple3) -> rule6))]
("Anne" "is" "quiet" "-")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
@0: Anne is big.[(triple1)] Anne is round.[(triple2)] Anne is white.[(triple3)] Dave is big.[(triple4 OR ((triple8 triple5) -> rule3))] Dave is kind.[(triple5 OR ((((triple4) -> rule4)) -> rule5))] Dave is quiet.[(triple6 OR ((triple5 triple9) -> rule6) OR ((((((triple4) -> rule4)) -> rule5) triple9) -> rule6))] Dave is red.[(triple7 OR ((triple4) -> rule1) OR ((((triple4) -> rule4)) -> rule2) OR ((((triple8 triple5) -> rule3)) -> rule1) OR ((((((triple8 triple5) -> rule3)) -> rule4)) -> rule2))] Dave is round.[(triple8)] Dave is white.[(triple9)] Gary is big.[(triple10 OR ((triple14 triple11) -> rule3))] Gary is kind.[(triple11 OR ((((triple10) -> rule4)) -> rule5))] Gary is not quiet.[(triple12)] Gary is not white.[(triple15)] Gary is red.[(triple13 OR ((triple10) -> rule1) OR ((((triple10) -> rule4)) -> rule2) OR ((((triple14 triple11) -> rule3)) -> rule1) OR ((((((triple14 triple11) -> rule3)) -> rule4)) -> rule2))] Gary is round.[(triple14)] @1: Anne is green.[(((triple1) -> rule4))] Anne is red.[(((triple1) -> rule1) OR ((((triple1) -> rule4)) -> rule2))] Dave is green.[(((triple4) -> rule4) OR ((((triple8 triple5) -> rule3)) -> rule4))] Gary is green.[(((triple10) -> rule4) OR ((((triple14 triple11) -> rule3)) -> rule4))] @2: Anne is kind.[(((((triple1) -> rule4)) -> rule5))] @3: Anne is quiet.[(((((((triple1) -> rule4)) -> rule5) triple3) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
((triple8 triple5) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple5
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
((triple5 triple9) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((((triple4) -> (rule4 % int3))) -> (rule5 % int2)) triple9) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
triple7
((triple4) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple8 triple5) -> (rule3 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((((triple8 triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
triple8
Dave is white.
("Dave" "is" "white" "+")
triple9
Gary is big.
("Gary" "is" "big" "+")
triple10
((triple14 triple11) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple11
((((triple10) -> (rule4 % int2))) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple12
Gary is not white.
("Gary" "is" "white" "-")
triple15
Gary is red.
("Gary" "is" "red" "+")
triple13
((triple10) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple14 triple11) -> (rule3 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((((triple14 triple11) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
triple14
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((triple4) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple8 triple5) -> (rule3 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((triple10) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple14 triple11) -> (rule3 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3