Anne is big. Anne is blue. Anne is furry. Anne is nice. Bob is big. Bob is blue. Bob is furry. Bob is kind. Bob is nice. Dave is big. Dave is blue. Dave is furry. Dave is kind. Dave is nice. Dave is red. Dave is round. Round things are red. If Anne is red then Anne is blue. If Bob is big then Bob is round. If Bob is furry then Bob is red. If something is round then it is nice. If something is big and furry then it is round.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If Anne is red then Anne is blue.
((("Anne" "is" "red" "+")) -> ("Anne" "is" "blue" "+"))
If Bob is big then Bob is round.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "round" "+"))
If Bob is furry then Bob is red.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "red" "+"))
If something is round then it is nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If something is big and furry then it is round.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
Dave is nice.
True
1
proof
[(triple14 OR ((triple16) -> rule5) OR ((((triple10 triple12) -> rule6)) -> rule5))]
("Dave" "is" "nice" "+")
triple14
((triple16) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple10 triple12) -> (rule6 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not blue.
False
1
inv-proof
[(triple11)]
("Dave" "is" "blue" "-")
triple11
Anne is round.
True
3
proof
[(((triple1 triple3) -> rule6))]
("Anne" "is" "round" "+")
((triple1 triple3) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple5) -> rule3) OR ((triple5 triple7) -> rule6))]
("Bob" "is" "round" "-")
((triple5) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple5 triple7) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Anne is red.
True
4
proof
[(((((triple1 triple3) -> rule6)) -> rule1))]
("Anne" "is" "red" "+")
((((triple1 triple3) -> (rule6 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not red.
False
4
inv-proof
[(((((triple1 triple3) -> rule6)) -> rule1))]
("Anne" "is" "red" "-")
((((triple1 triple3) -> (rule6 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
@0: Anne is big.[(triple1)] Anne is blue.[(triple2 OR ((((((triple1 triple3) -> rule6)) -> rule1)) -> rule2))] Anne is furry.[(triple3)] Anne is nice.[(triple4 OR ((((triple1 triple3) -> rule6)) -> rule5))] Bob is big.[(triple5)] Bob is blue.[(triple6)] Bob is furry.[(triple7)] Bob is kind.[(triple8)] Bob is nice.[(triple9 OR ((((triple5) -> rule3)) -> rule5) OR ((((triple5 triple7) -> rule6)) -> rule5))] Dave is big.[(triple10)] Dave is blue.[(triple11)] Dave is furry.[(triple12)] Dave is kind.[(triple13)] Dave is nice.[(triple14 OR ((triple16) -> rule5) OR ((((triple10 triple12) -> rule6)) -> rule5))] Dave is red.[(triple15 OR ((triple16) -> rule1) OR ((((triple10 triple12) -> rule6)) -> rule1))] Dave is round.[(triple16 OR ((triple10 triple12) -> rule6))] @1: Anne is round.[(((triple1 triple3) -> rule6))] Bob is red.[(((triple7) -> rule4) OR ((((triple5) -> rule3)) -> rule1) OR ((((triple5 triple7) -> rule6)) -> rule1))] Bob is round.[(((triple5) -> rule3) OR ((triple5 triple7) -> rule6))] @2: Anne is red.[(((((triple1 triple3) -> rule6)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((((((triple1 triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
((((triple1 triple3) -> (rule6 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
triple5
Bob is blue.
("Bob" "is" "blue" "+")
triple6
Bob is furry.
("Bob" "is" "furry" "+")
triple7
Bob is kind.
("Bob" "is" "kind" "+")
triple8
Bob is nice.
("Bob" "is" "nice" "+")
triple9
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple5 triple7) -> (rule6 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
triple10
Dave is blue.
("Dave" "is" "blue" "+")
triple11
Dave is furry.
("Dave" "is" "furry" "+")
triple12
Dave is kind.
("Dave" "is" "kind" "+")
triple13
Dave is nice.
("Dave" "is" "nice" "+")
triple14
((triple16) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple10 triple12) -> (rule6 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple15
((triple16) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple10 triple12) -> (rule6 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
triple16
((triple10 triple12) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple1 triple3) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple7) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple5 triple7) -> (rule6 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((triple5) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple5 triple7) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1 triple3) -> (rule6 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2