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