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