Bob is green. Bob is kind. Bob is quiet. Bob is rough. Bob is round. Dave is blue. Dave is green. Dave is kind. Dave is quiet. Dave is rough. Dave is round. Dave is smart. Kind, rough people are round. If someone is blue then they are smart. All kind people are round. If Dave is smart then Dave is round. If someone is rough then they are green. If someone is smart then they are quiet. Blue, round people are kind. Round people are blue.
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Kind, rough people are round.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If someone is blue then they are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
All kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If Dave is smart then Dave is round.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "round" "+"))
If someone is rough then they are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If someone is smart then they are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Blue, round people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
Round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Bob is rough.
True
1
proof
[(triple4)]
("Bob" "is" "rough" "+")
triple4
Bob is not quiet.
False
1
inv-proof
[(triple3 OR ((((((triple5) -> rule8)) -> rule2)) -> rule6) OR ((((((((triple2) -> rule3)) -> rule8)) -> rule2)) -> rule6) OR ((((((((triple2 triple4) -> rule1)) -> rule8)) -> rule2)) -> rule6))]
("Bob" "is" "quiet" "-")
triple3
((((((triple5) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((((((triple2) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
((((((((triple2 triple4) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is blue.
True
2
proof
[(((triple5) -> rule8) OR ((((triple2) -> rule3)) -> rule8) OR ((((triple2 triple4) -> rule1)) -> rule8))]
("Bob" "is" "blue" "+")
((triple5) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple2 triple4) -> (rule1 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not blue.
False
2
inv-proof
[(((triple5) -> rule8) OR ((((triple2) -> rule3)) -> rule8) OR ((((triple2 triple4) -> rule1)) -> rule8))]
("Bob" "is" "blue" "-")
((triple5) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple2 triple4) -> (rule1 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is smart.
True
3
proof
[(((((triple5) -> rule8)) -> rule2) OR ((((((triple2) -> rule3)) -> rule8)) -> rule2) OR ((((((triple2 triple4) -> rule1)) -> rule8)) -> rule2))]
("Bob" "is" "smart" "+")
((((triple5) -> (rule8 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((((triple2 triple4) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not smart.
False
3
inv-proof
[(((((triple5) -> rule8)) -> rule2) OR ((((((triple2) -> rule3)) -> rule8)) -> rule2) OR ((((((triple2 triple4) -> rule1)) -> rule8)) -> rule2))]
("Bob" "is" "smart" "-")
((((triple5) -> (rule8 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((((triple2 triple4) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
@0: Bob is green.[(triple1 OR ((triple4) -> rule5))] Bob is kind.[(triple2 OR ((((triple5) -> rule8) triple5) -> rule7))] Bob is quiet.[(triple3 OR ((((((triple5) -> rule8)) -> rule2)) -> rule6) OR ((((((((triple2) -> rule3)) -> rule8)) -> rule2)) -> rule6) OR ((((((((triple2 triple4) -> rule1)) -> rule8)) -> rule2)) -> rule6))] Bob is rough.[(triple4)] Bob is round.[(triple5 OR ((triple2) -> rule3) OR ((triple2 triple4) -> rule1))] Dave is blue.[(triple6 OR ((triple11) -> rule8) OR ((((triple12) -> rule4)) -> rule8) OR ((((triple8) -> rule3)) -> rule8) OR ((((triple8 triple10) -> rule1)) -> rule8))] Dave is green.[(triple7 OR ((triple10) -> rule5))] Dave is kind.[(triple8 OR ((triple6 triple11) -> rule7) OR ((triple6 ((triple12) -> rule4)) -> rule7) OR ((((triple11) -> rule8) triple11) -> rule7) OR ((((triple11) -> rule8) ((triple12) -> rule4)) -> rule7) OR ((triple6 ((((triple6) -> rule2)) -> rule4)) -> rule7) OR ((((((triple12) -> rule4)) -> rule8) triple11) -> rule7) OR ((((triple11) -> rule8) ((((triple6) -> rule2)) -> rule4)) -> rule7) OR ((((((triple12) -> rule4)) -> rule8) ((triple12) -> rule4)) -> rule7) OR ((((((triple12) -> rule4)) -> rule8) ((((triple6) -> rule2)) -> rule4)) -> rule7))] Dave is quiet.[(triple9 OR ((triple12) -> rule6) OR ((((triple6) -> rule2)) -> rule6) OR ((((((triple11) -> rule8)) -> rule2)) -> rule6) OR ((((((((triple8) -> rule3)) -> rule8)) -> rule2)) -> rule6) OR ((((((((triple8 triple10) -> rule1)) -> rule8)) -> rule2)) -> rule6))] Dave is rough.[(triple10)] Dave is round.[(triple11 OR ((triple12) -> rule4) OR ((triple8) -> rule3) OR ((triple8 triple10) -> rule1) OR ((((triple6) -> rule2)) -> rule4))] Dave is smart.[(triple12 OR ((triple6) -> rule2) OR ((((triple11) -> rule8)) -> rule2) OR ((((((triple8) -> rule3)) -> rule8)) -> rule2) OR ((((((triple8 triple10) -> rule1)) -> rule8)) -> rule2))] @1: Bob is blue.[(((triple5) -> rule8) OR ((((triple2) -> rule3)) -> rule8) OR ((((triple2 triple4) -> rule1)) -> rule8))] @2: Bob is smart.[(((((triple5) -> rule8)) -> rule2) OR ((((((triple2) -> rule3)) -> rule8)) -> rule2) OR ((((((triple2 triple4) -> rule1)) -> rule8)) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
((triple4) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
((((triple5) -> (rule8 % int2)) triple5) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((((((triple5) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((((((triple2) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
((((((((triple2 triple4) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
((triple2) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple2 triple4) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple6
((triple11) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple12) -> (rule4 % int2))) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple8) -> (rule3 % int2))) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple8 triple10) -> (rule1 % int2))) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple7
((triple10) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple8
((triple6 triple11) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple6 ((triple12) -> (rule4 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple11) -> (rule8 % int2)) triple11) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple11) -> (rule8 % int3)) ((triple12) -> (rule4 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((triple6 ((((triple6) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((((((triple12) -> (rule4 % int3))) -> (rule8 % int2)) triple11) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((triple11) -> (rule8 % int4)) ((((triple6) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
((((((triple12) -> (rule4 % int3))) -> (rule8 % int2)) ((triple12) -> (rule4 % int3))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((((triple12) -> (rule4 % int4))) -> (rule8 % int3)) ((((triple6) -> (rule2 % int2))) -> (rule4 % int4))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple9
((triple12) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((((triple11) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((((((triple8) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((((((triple8 triple10) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
triple10
Dave is round.
("Dave" "is" "round" "+")
triple11
((triple12) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple8) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple8 triple10) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple12
((triple6) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple11) -> (rule8 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((((triple8) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((((triple8 triple10) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
((triple5) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple2 triple4) -> (rule1 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((triple5) -> (rule8 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((((triple2 triple4) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3