Anne is blue. Anne is quiet. Anne is white. Anne is young. Bob is quiet. Bob is rough. Bob is white. Bob is young. Gary is blue. Gary is kind. Gary is quiet. Gary is rough. Gary is round. Gary is white. Gary is young. If something is quiet and rough then it is white. All white things are rough. If something is round then it is white. If something is rough and young then it is round. If something is blue and quiet then it is white. All white things are quiet. If Anne is kind then Anne is rough. If something is round and young then it is kind.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is quiet and rough then it is white.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
All white things are rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If something is round then it is white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If something is rough and young then it is round.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If something is blue and quiet then it is white.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
All white things are quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If Anne is kind then Anne is rough.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "rough" "+"))
If something is round and young then it is kind.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
Gary is quiet.
True
1
proof
[(triple11 OR ((triple14) -> rule6) OR ((((triple13) -> rule3)) -> rule6) OR ((((((triple12 triple15) -> rule4)) -> rule3)) -> rule6))]
("Gary" "is" "quiet" "+")
triple11
((triple14) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple13) -> (rule3 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((((triple12 triple15) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is not rough.
False
1
inv-proof
[(triple12 OR ((triple14) -> rule2) OR ((((triple13) -> rule3)) -> rule2) OR ((((triple9 triple11) -> rule5)) -> rule2))]
("Gary" "is" "rough" "-")
triple12
((triple14) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple13) -> (rule3 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((triple9 triple11) -> (rule5 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Anne is rough.
True
2
proof
[(((triple3) -> rule2) OR ((((triple1 triple2) -> rule5)) -> rule2))]
("Anne" "is" "rough" "+")
((triple3) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple1 triple2) -> (rule5 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is not rough.
False
2
inv-proof
[(((triple3) -> rule2) OR ((((triple1 triple2) -> rule5)) -> rule2))]
("Anne" "is" "rough" "-")
((triple3) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple1 triple2) -> (rule5 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Bob is kind.
True
5
proof
[(((((triple6 triple8) -> rule4) triple8) -> rule8) OR ((((((triple7) -> rule2) triple8) -> rule4) triple8) -> rule8))]
("Bob" "is" "kind" "+")
((((triple6 triple8) -> (rule4 % int2)) triple8) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((((triple7) -> (rule2 % int3)) triple8) -> (rule4 % int2)) triple8) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not kind.
False
5
inv-proof
[(((((triple6 triple8) -> rule4) triple8) -> rule8) OR ((((((triple7) -> rule2) triple8) -> rule4) triple8) -> rule8))]
("Bob" "is" "kind" "-")
((((triple6 triple8) -> (rule4 % int2)) triple8) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((((triple7) -> (rule2 % int3)) triple8) -> (rule4 % int2)) triple8) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Anne is kind.
True
6
proof
[(((((((triple3) -> rule2) triple4) -> rule4) triple4) -> rule8) OR ((((((((triple1 triple2) -> rule5)) -> rule2) triple4) -> rule4) triple4) -> rule8))]
("Anne" "is" "kind" "+")
((((((triple3) -> (rule2 % int3)) triple4) -> (rule4 % int2)) triple4) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((((((((triple1 triple2) -> (rule5 % int4))) -> (rule2 % int3)) triple4) -> (rule4 % int2)) triple4) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is not kind.
False
6
inv-proof
[(((((((triple3) -> rule2) triple4) -> rule4) triple4) -> rule8) OR ((((((((triple1 triple2) -> rule5)) -> rule2) triple4) -> rule4) triple4) -> rule8))]
("Anne" "is" "kind" "-")
((((((triple3) -> (rule2 % int3)) triple4) -> (rule4 % int2)) triple4) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((((((((triple1 triple2) -> (rule5 % int4))) -> (rule2 % int3)) triple4) -> (rule4 % int2)) triple4) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
@0: Anne is blue.[(triple1)] Anne is quiet.[(triple2 OR ((triple3) -> rule6))] Anne is white.[(triple3 OR ((triple1 triple2) -> rule5))] Anne is young.[(triple4)] Bob is quiet.[(triple5 OR ((triple7) -> rule6) OR ((((((triple6 triple8) -> rule4)) -> rule3)) -> rule6))] Bob is rough.[(triple6 OR ((triple7) -> rule2))] Bob is white.[(triple7 OR ((triple5 triple6) -> rule1) OR ((((triple6 triple8) -> rule4)) -> rule3))] Bob is young.[(triple8)] Gary is blue.[(triple9)] Gary is kind.[(triple10 OR ((triple13 triple15) -> rule8) OR ((((triple12 triple15) -> rule4) triple15) -> rule8) OR ((((((triple14) -> rule2) triple15) -> rule4) triple15) -> rule8) OR ((((((((triple9 triple11) -> rule5)) -> rule2) triple15) -> rule4) triple15) -> rule8))] Gary is quiet.[(triple11 OR ((triple14) -> rule6) OR ((((triple13) -> rule3)) -> rule6) OR ((((((triple12 triple15) -> rule4)) -> rule3)) -> rule6))] Gary is rough.[(triple12 OR ((triple14) -> rule2) OR ((((triple13) -> rule3)) -> rule2) OR ((((triple9 triple11) -> rule5)) -> rule2))] Gary is round.[(triple13 OR ((triple12 triple15) -> rule4) OR ((((triple14) -> rule2) triple15) -> rule4) OR ((((((triple9 triple11) -> rule5)) -> rule2) triple15) -> rule4))] Gary is white.[(triple14 OR ((triple13) -> rule3) OR ((triple11 triple12) -> rule1) OR ((triple9 triple11) -> rule5) OR ((((triple12 triple15) -> rule4)) -> rule3))] Gary is young.[(triple15)] @1: Anne is rough.[(((triple3) -> rule2) OR ((((triple1 triple2) -> rule5)) -> rule2))] Bob is round.[(((triple6 triple8) -> rule4) OR ((((triple7) -> rule2) triple8) -> rule4))] @2: Anne is round.[(((((triple3) -> rule2) triple4) -> rule4) OR ((((((triple1 triple2) -> rule5)) -> rule2) triple4) -> rule4))] Bob is kind.[(((((triple6 triple8) -> rule4) triple8) -> rule8) OR ((((((triple7) -> rule2) triple8) -> rule4) triple8) -> rule8))] @3: Anne is kind.[(((((((triple3) -> rule2) triple4) -> rule4) triple4) -> rule8) OR ((((((((triple1 triple2) -> rule5)) -> rule2) triple4) -> rule4) triple4) -> rule8))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
((triple3) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple3
((triple1 triple2) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((triple7) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((((triple6 triple8) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
triple6
((triple7) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple7
((triple5 triple6) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple6 triple8) -> (rule4 % int2))) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple9
Gary is kind.
("Gary" "is" "kind" "+")
triple10
((triple13 triple15) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple12 triple15) -> (rule4 % int2)) triple15) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((((triple14) -> (rule2 % int3)) triple15) -> (rule4 % int2)) triple15) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((((((((triple9 triple11) -> (rule5 % int4))) -> (rule2 % int3)) triple15) -> (rule4 % int2)) triple15) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple11
((triple14) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple13) -> (rule3 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((((triple12 triple15) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
triple12
((triple14) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple13) -> (rule3 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((triple9 triple11) -> (rule5 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
triple13
((triple12 triple15) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple14) -> (rule2 % int2)) triple15) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((((triple9 triple11) -> (rule5 % int3))) -> (rule2 % int2)) triple15) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
triple14
((triple13) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple11 triple12) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple9 triple11) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((triple12 triple15) -> (rule4 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
triple15
Anne is rough.
("Anne" "is" "rough" "+")
((triple3) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple1 triple2) -> (rule5 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((triple6 triple8) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple7) -> (rule2 % int2)) triple8) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((((triple3) -> (rule2 % int2)) triple4) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((((triple1 triple2) -> (rule5 % int3))) -> (rule2 % int2)) triple4) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
((((triple6 triple8) -> (rule4 % int2)) triple8) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((((triple7) -> (rule2 % int3)) triple8) -> (rule4 % int2)) triple8) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
((((((triple3) -> (rule2 % int3)) triple4) -> (rule4 % int2)) triple4) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((((((((triple1 triple2) -> (rule5 % int4))) -> (rule2 % int3)) triple4) -> (rule4 % int2)) triple4) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4