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