Bob is big. Bob is cold. Bob is green. Bob is round. Bob is white. Dave is big. Dave is cold. Dave is green. Dave is quiet. Dave is rough. Dave is round. Dave is white. If something is cold then it is quiet. All white, quiet things are cold.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
If something is cold then it is quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
All white, quiet things are cold.
((("something" "is" "white" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
Bob is green.
True
1
proof
[(triple3)]
("Bob" "is" "green" "+")
triple3
Bob is not round.
False
1
inv-proof
[(triple4)]
("Bob" "is" "round" "-")
triple4
@0: Bob is big.[(triple1)] Bob is cold.[(triple2)] Bob is green.[(triple3)] Bob is round.[(triple4)] Bob is white.[(triple5)] Dave is big.[(triple6)] Dave is cold.[(triple7 OR ((triple12 triple9) -> rule2))] Dave is green.[(triple8)] Dave is quiet.[(triple9 OR ((triple7) -> rule1))] Dave is rough.[(triple10)] Dave is round.[(triple11)] Dave is white.[(triple12)] @1: Bob is quiet.[(((triple2) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is cold.
("Dave" "is" "cold" "+")
triple7
((triple12 triple9) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple8
Dave is quiet.
("Dave" "is" "quiet" "+")
triple9
((triple7) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple10
Dave is round.
("Dave" "is" "round" "+")
triple11
Dave is white.
("Dave" "is" "white" "+")
triple12
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1