Bob is furry. Bob is green. Bob is red. Bob is round. Bob is smart. Charlie is blue. Charlie is furry. Charlie is green. Charlie is nice. Charlie is red. Charlie is round. Charlie is smart. If Bob is red then Bob is blue.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
If Bob is red then Bob is blue.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "blue" "+"))
Bob is smart.
True
1
proof
[(triple5)]
("Bob" "is" "smart" "+")
triple5
Bob is not red.
False
1
inv-proof
[(triple3)]
("Bob" "is" "red" "-")
triple3
@0: Bob is furry.[(triple1)] Bob is green.[(triple2)] Bob is red.[(triple3)] Bob is round.[(triple4)] Bob is smart.[(triple5)] Charlie is blue.[(triple6)] Charlie is furry.[(triple7)] Charlie is green.[(triple8)] Charlie is nice.[(triple9)] Charlie is red.[(triple10)] Charlie is round.[(triple11)] Charlie is smart.[(triple12)] @1: Bob is blue.[(((triple3) -> rule1))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
triple8
Charlie is nice.
("Charlie" "is" "nice" "+")
triple9
Charlie is red.
("Charlie" "is" "red" "+")
triple10
Charlie is round.
("Charlie" "is" "round" "+")
triple11
Charlie is smart.
("Charlie" "is" "smart" "+")
triple12
Bob is blue.
("Bob" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1