Bob is blue. Bob is green. Bob is kind. Bob is red. Bob is not rough. Bob is round. Bob is smart. Charlie is blue. Charlie is not green. Charlie is kind. Charlie is red. Charlie is rough. Charlie is round. Charlie is smart. If someone is round and not blue then they are green. If someone is smart then they are round. If Bob is round and Bob is rough then Bob is kind.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
If someone is round and not blue then they are green.
((("someone" "is" "round" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "green" "+"))
If someone is smart then they are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If Bob is round and Bob is rough then Bob is kind.
((("Bob" "is" "round" "+") ("Bob" "is" "rough" "+")) -> ("Bob" "is" "kind" "+"))
Charlie is blue.
True
1
proof
[(triple8)]
("Charlie" "is" "blue" "+")
triple8
Bob is not round.
False
1
inv-proof
[(triple6 OR ((triple7) -> rule2))]
("Bob" "is" "round" "-")
triple6
((triple7) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
@0: Bob is blue.[(triple1)] Bob is green.[(triple2)] Bob is kind.[(triple3)] Bob is not rough.[(triple5)] Bob is red.[(triple4)] Bob is round.[(triple6 OR ((triple7) -> rule2))] Bob is smart.[(triple7)] Charlie is blue.[(triple8)] Charlie is kind.[(triple10)] Charlie is not green.[(triple9)] Charlie is red.[(triple11)] Charlie is rough.[(triple12)] Charlie is round.[(triple13 OR ((triple14) -> rule2))] Charlie is smart.[(triple14)]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is not rough.
("Bob" "is" "rough" "-")
triple5
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple6
((triple7) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple7
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
Charlie is kind.
("Charlie" "is" "kind" "+")
triple10
Charlie is not green.
("Charlie" "is" "green" "-")
triple9
Charlie is red.
("Charlie" "is" "red" "+")
triple11
Charlie is rough.
("Charlie" "is" "rough" "+")
triple12
Charlie is round.
("Charlie" "is" "round" "+")
triple13
((triple14) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple14