Bob is blue. Bob is green. Bob is nice. Bob is red. Bob is rough. Bob is round. Bob is white. Charlie is blue. Charlie is green. Charlie is nice. Charlie is red. Charlie is rough. Charlie is round. Charlie is white. If something is rough then it is round. If something is rough then it is red. All round, red things are white.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
If something is rough then it is round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is rough then it is red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
All round, red things are white.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
Charlie is white.
True
1
proof
[(triple14 OR ((triple13 triple11) -> rule3) OR ((triple13 ((triple12) -> rule2)) -> rule3) OR ((((triple12) -> rule1) triple11) -> rule3) OR ((((triple12) -> rule1) ((triple12) -> rule2)) -> rule3))]
("Charlie" "is" "white" "+")
triple14
((triple13 triple11) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple13 ((triple12) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((triple12) -> (rule1 % int2)) triple11) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((triple12) -> (rule1 % int3)) ((triple12) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Bob is not rough.
False
1
inv-proof
[(triple5)]
("Bob" "is" "rough" "-")
triple5
@0: Bob is blue.[(triple1)] Bob is green.[(triple2)] Bob is nice.[(triple3)] Bob is red.[(triple4 OR ((triple5) -> rule2))] Bob is rough.[(triple5)] Bob is round.[(triple6 OR ((triple5) -> rule1))] Bob is white.[(triple7 OR ((triple6 triple4) -> rule3) OR ((triple6 ((triple5) -> rule2)) -> rule3) OR ((((triple5) -> rule1) triple4) -> rule3) OR ((((triple5) -> rule1) ((triple5) -> rule2)) -> rule3))] Charlie is blue.[(triple8)] Charlie is green.[(triple9)] Charlie is nice.[(triple10)] Charlie is red.[(triple11 OR ((triple12) -> rule2))] Charlie is rough.[(triple12)] Charlie is round.[(triple13 OR ((triple12) -> rule1))] Charlie is white.[(triple14 OR ((triple13 triple11) -> rule3) OR ((triple13 ((triple12) -> rule2)) -> rule3) OR ((((triple12) -> rule1) triple11) -> rule3) OR ((((triple12) -> rule1) ((triple12) -> rule2)) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple5) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
((triple5) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple7
((triple6 triple4) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple6 ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple5) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple5) -> (rule1 % int3)) ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
Charlie is green.
("Charlie" "is" "green" "+")
triple9
Charlie is nice.
("Charlie" "is" "nice" "+")
triple10
Charlie is red.
("Charlie" "is" "red" "+")
triple11
((triple12) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple12
Charlie is round.
("Charlie" "is" "round" "+")
triple13
((triple12) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple14
((triple13 triple11) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple13 ((triple12) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((triple12) -> (rule1 % int2)) triple11) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((triple12) -> (rule1 % int3)) ((triple12) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3