Bob is blue. Bob is cold. Bob is green. Bob is quiet. Bob is rough. Bob is round. Bob is smart. All blue people are rough. If someone is smart then they are quiet. Cold people are green. Cold, blue people are green. Round people are blue. All smart people are round.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
All blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If someone is smart then they are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Cold people are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
Cold, blue people are green.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
All smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
Bob is green.
True
1
proof
[(triple3 OR ((triple2) -> rule3) OR ((triple2 triple1) -> rule4) OR ((triple2 ((triple6) -> rule5)) -> rule4) OR ((triple2 ((((triple7) -> rule6)) -> rule5)) -> rule4))]
("Bob" "is" "green" "+")
triple3
((triple2) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple2 triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple2 ((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((triple2 ((((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not blue.
False
1
inv-proof
[(triple1 OR ((triple6) -> rule5) OR ((((triple7) -> rule6)) -> rule5))]
("Bob" "is" "blue" "-")
triple1
((triple6) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
@0: Bob is blue.[(triple1 OR ((triple6) -> rule5) OR ((((triple7) -> rule6)) -> rule5))] Bob is cold.[(triple2)] Bob is green.[(triple3 OR ((triple2) -> rule3) OR ((triple2 triple1) -> rule4) OR ((triple2 ((triple6) -> rule5)) -> rule4) OR ((triple2 ((((triple7) -> rule6)) -> rule5)) -> rule4))] Bob is quiet.[(triple4 OR ((triple7) -> rule2))] Bob is rough.[(triple5 OR ((triple1) -> rule1) OR ((((triple6) -> rule5)) -> rule1) OR ((((((triple7) -> rule6)) -> rule5)) -> rule1))] Bob is round.[(triple6 OR ((triple7) -> rule6))] Bob is smart.[(triple7)]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple6) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
((triple2) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple2 triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple2 ((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((triple2 ((((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple7) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
triple6
((triple7) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple7