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