Anne is big. Anne is blue. Anne is cold. Anne is furry. Anne is green. Anne is red. Anne is round. Dave is big. Dave is blue. Dave is cold. Dave is furry. Dave is green. Dave is red. Dave is round. Big, blue things are cold. Blue, round things are green. Round things are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Big, blue things are cold.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Blue, round things are green.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
Round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Anne is round.
True
1
proof
[(triple7)]
("Anne" "is" "round" "+")
triple7
Dave is not big.
False
1
inv-proof
[(triple8 OR ((triple14) -> rule3))]
("Dave" "is" "big" "-")
triple8
((triple14) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
@0: Anne is big.[(triple1 OR ((triple7) -> rule3))] Anne is blue.[(triple2)] Anne is cold.[(triple3 OR ((triple1 triple2) -> rule1) OR ((((triple7) -> rule3) triple2) -> rule1))] Anne is furry.[(triple4)] Anne is green.[(triple5 OR ((triple2 triple7) -> rule2))] Anne is red.[(triple6)] Anne is round.[(triple7)] Dave is big.[(triple8 OR ((triple14) -> rule3))] Dave is blue.[(triple9)] Dave is cold.[(triple10 OR ((triple8 triple9) -> rule1) OR ((((triple14) -> rule3) triple9) -> rule1))] Dave is furry.[(triple11)] Dave is green.[(triple12 OR ((triple9 triple14) -> rule2))] Dave is red.[(triple13)] Dave is round.[(triple14)]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple7) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is cold.
("Anne" "is" "cold" "+")
triple3
((triple1 triple2) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple7) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
triple4
Anne is green.
("Anne" "is" "green" "+")
triple5
((triple2 triple7) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple6
Anne is round.
("Anne" "is" "round" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
((triple14) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple9
Dave is cold.
("Dave" "is" "cold" "+")
triple10
((triple8 triple9) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple14) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple11
Dave is green.
("Dave" "is" "green" "+")
triple12
((triple9 triple14) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple13
Dave is round.
("Dave" "is" "round" "+")
triple14