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