Bob is blue. Bob is furry. Bob is quiet. Bob is red. Bob is rough. Bob is white. Dave is blue. Dave is quiet. Dave is red. Dave is rough. If Dave is blue then Dave is red. Furry, rough people are red. Nice, furry people are red. All blue people are furry. All red people are blue. If someone is furry and quiet then they are nice. Nice, rough people are red. If Dave is rough then Dave is red.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
If Dave is blue then Dave is red.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "red" "+"))
Furry, rough people are red.
((("someone" "is" "furry" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
Nice, furry people are red.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
All blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
All red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is furry and quiet then they are nice.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Nice, rough people are red.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If Dave is rough then Dave is red.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "red" "+"))
Dave is rough.
True
1
proof
[(triple10)]
("Dave" "is" "rough" "+")
triple10
Dave is not quiet.
False
1
inv-proof
[(triple8)]
("Dave" "is" "quiet" "-")
triple8
Bob is nice.
True
3
proof
[(((triple2 triple3) -> rule6) OR ((((triple1) -> rule4) triple3) -> rule6) OR ((((((triple4) -> rule5)) -> rule4) triple3) -> rule6))]
("Bob" "is" "nice" "+")
((triple2 triple3) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple1) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple4) -> (rule5 % int3))) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Dave is not furry.
False
2
inv-proof
[(((triple7) -> rule4) OR ((((triple9) -> rule5)) -> rule4) OR ((((((triple10) -> rule8)) -> rule5)) -> rule4))]
("Dave" "is" "furry" "-")
((triple7) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple9) -> (rule5 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((((triple10) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is nice.
True
4
proof
[(((((triple7) -> rule4) triple8) -> rule6) OR ((((((triple9) -> rule5)) -> rule4) triple8) -> rule6) OR ((((((((triple10) -> rule8)) -> rule5)) -> rule4) triple8) -> rule6))]
("Dave" "is" "nice" "+")
((((triple7) -> (rule4 % int2)) triple8) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((((triple9) -> (rule5 % int3))) -> (rule4 % int2)) triple8) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((((((triple10) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) triple8) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is not nice.
False
4
inv-proof
[(((((triple7) -> rule4) triple8) -> rule6) OR ((((((triple9) -> rule5)) -> rule4) triple8) -> rule6) OR ((((((((triple10) -> rule8)) -> rule5)) -> rule4) triple8) -> rule6))]
("Dave" "is" "nice" "-")
((((triple7) -> (rule4 % int2)) triple8) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((((triple9) -> (rule5 % int3))) -> (rule4 % int2)) triple8) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((((((triple10) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) triple8) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
@0: Bob is blue.[(triple1 OR ((triple4) -> rule5) OR ((((triple2 triple5) -> rule2)) -> rule5) OR ((((((triple2 triple3) -> rule6) triple2) -> rule3)) -> rule5) OR ((((((triple2 triple3) -> rule6) triple5) -> rule7)) -> rule5))] Bob is furry.[(triple2 OR ((triple1) -> rule4) OR ((((triple4) -> rule5)) -> rule4))] Bob is quiet.[(triple3)] Bob is red.[(triple4 OR ((triple2 triple5) -> rule2) OR ((((triple1) -> rule4) triple5) -> rule2) OR ((((triple2 triple3) -> rule6) triple2) -> rule3) OR ((((triple2 triple3) -> rule6) triple5) -> rule7) OR ((((triple2 triple3) -> rule6) ((triple1) -> rule4)) -> rule3) OR ((((((triple1) -> rule4) triple3) -> rule6) triple2) -> rule3) OR ((((((triple1) -> rule4) triple3) -> rule6) triple5) -> rule7) OR ((((((triple1) -> rule4) triple3) -> rule6) ((triple1) -> rule4)) -> rule3))] Bob is rough.[(triple5)] Bob is white.[(triple6)] Dave is blue.[(triple7 OR ((triple9) -> rule5) OR ((((triple10) -> rule8)) -> rule5))] Dave is quiet.[(triple8)] Dave is red.[(triple9 OR ((triple10) -> rule8) OR ((triple7) -> rule1) OR ((((triple7) -> rule4) triple10) -> rule2) OR ((((((triple7) -> rule4) triple8) -> rule6) triple10) -> rule7) OR ((((((triple7) -> rule4) triple8) -> rule6) ((triple7) -> rule4)) -> rule3))] Dave is rough.[(triple10)] @1: Bob is nice.[(((triple2 triple3) -> rule6) OR ((((triple1) -> rule4) triple3) -> rule6) OR ((((((triple4) -> rule5)) -> rule4) triple3) -> rule6))] Dave is furry.[(((triple7) -> rule4) OR ((((triple9) -> rule5)) -> rule4) OR ((((((triple10) -> rule8)) -> rule5)) -> rule4))] @2: Dave is nice.[(((((triple7) -> rule4) triple8) -> rule6) OR ((((((triple9) -> rule5)) -> rule4) triple8) -> rule6) OR ((((((((triple10) -> rule8)) -> rule5)) -> rule4) triple8) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple4) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple2 triple5) -> (rule2 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((((triple2 triple3) -> (rule6 % int3)) triple2) -> (rule3 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((((triple2 triple3) -> (rule6 % int3)) triple5) -> (rule7 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple1) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple2 triple5) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple1) -> (rule4 % int2)) triple5) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple2 triple3) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple2 triple3) -> (rule6 % int2)) triple5) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple2 triple3) -> (rule6 % int3)) ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((((triple1) -> (rule4 % int3)) triple3) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((((triple1) -> (rule4 % int3)) triple3) -> (rule6 % int2)) triple5) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((((triple1) -> (rule4 % int3)) triple3) -> (rule6 % int2)) ((triple1) -> (rule4 % int3))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Dave is blue.
("Dave" "is" "blue" "+")
triple7
((triple9) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple10) -> (rule8 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
Dave is red.
("Dave" "is" "red" "+")
triple9
((triple10) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple7) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple7) -> (rule4 % int2)) triple10) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((((triple7) -> (rule4 % int3)) triple8) -> (rule6 % int2)) triple10) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
((((((triple7) -> (rule4 % int3)) triple8) -> (rule6 % int2)) ((triple7) -> (rule4 % int3))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
triple10
Bob is nice.
("Bob" "is" "nice" "+")
((triple2 triple3) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple1) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple4) -> (rule5 % int3))) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
((triple7) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple9) -> (rule5 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((((triple10) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((((triple7) -> (rule4 % int2)) triple8) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((((triple9) -> (rule5 % int3))) -> (rule4 % int2)) triple8) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((((((triple10) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) triple8) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4