Bob is big. Bob is green. Bob is quiet. Bob is red. Bob is round. Bob is smart. Bob is white. Dave is big. Dave is green. Dave is quiet. Dave is red. Dave is round. Dave is smart. Dave is white. If something is smart and red then it is big. If something is green and quiet then it is red. If something is quiet and green then it is white.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
If something is smart and red then it is big.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is green and quiet then it is red.
((("something" "is" "green" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If something is quiet and green then it is white.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
Bob is red.
True
1
proof
[(triple4 OR ((triple2 triple3) -> rule2))]
("Bob" "is" "red" "+")
triple4
((triple2 triple3) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Dave is not green.
False
1
inv-proof
[(triple9)]
("Dave" "is" "green" "-")
triple9
@0: Bob is big.[(triple1 OR ((triple6 triple4) -> rule1) OR ((triple6 ((triple2 triple3) -> rule2)) -> rule1))] Bob is green.[(triple2)] Bob is quiet.[(triple3)] Bob is red.[(triple4 OR ((triple2 triple3) -> rule2))] Bob is round.[(triple5)] Bob is smart.[(triple6)] Bob is white.[(triple7 OR ((triple3 triple2) -> rule3))] Dave is big.[(triple8 OR ((triple13 triple11) -> rule1) OR ((triple13 ((triple9 triple10) -> rule2)) -> rule1))] Dave is green.[(triple9)] Dave is quiet.[(triple10)] Dave is red.[(triple11 OR ((triple9 triple10) -> rule2))] Dave is round.[(triple12)] Dave is smart.[(triple13)] Dave is white.[(triple14 OR ((triple10 triple9) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple6 triple4) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple6 ((triple2 triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple2 triple3) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7
((triple3 triple2) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple8
((triple13 triple11) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple13 ((triple9 triple10) -> (rule2 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple9
Dave is quiet.
("Dave" "is" "quiet" "+")
triple10
Dave is red.
("Dave" "is" "red" "+")
triple11
((triple9 triple10) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple12
Dave is smart.
("Dave" "is" "smart" "+")
triple13
Dave is white.
("Dave" "is" "white" "+")
triple14
((triple10 triple9) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1