Bob is blue. Bob is cold. Bob is furry. Bob is green. Bob is quiet. Bob is round. Bob is young. Erin is blue. Erin is cold. Erin is green. Erin is quiet. Erin is young. All furry, round people are quiet. Quiet people are blue. Young, cold people are quiet. Young people are furry. If Bob is blue and Bob is green then Bob is quiet. All furry people are young.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is young.
("Erin" "is" "young" "+")
All furry, round people are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
Quiet people are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
Young, cold people are quiet.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
Young people are furry.
((("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
If Bob is blue and Bob is green then Bob is quiet.
((("Bob" "is" "blue" "+") ("Bob" "is" "green" "+")) -> ("Bob" "is" "quiet" "+"))
All furry people are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
Bob is round.
True
1
proof
[(triple6)]
("Bob" "is" "round" "+")
triple6
Bob is not quiet.
False
1
inv-proof
[(triple5 OR ((triple1 triple4) -> rule5) OR ((triple3 triple6) -> rule1) OR ((triple7 triple2) -> rule3) OR ((((triple3) -> rule6) triple2) -> rule3) OR ((((triple7) -> rule4) triple6) -> rule1))]
("Bob" "is" "quiet" "-")
triple5
((triple1 triple4) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple3 triple6) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple7 triple2) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple3) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple7) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
@0: Bob is blue.[(triple1 OR ((triple5) -> rule2) OR ((((triple3 triple6) -> rule1)) -> rule2) OR ((((triple7 triple2) -> rule3)) -> rule2) OR ((((((triple3) -> rule6) triple2) -> rule3)) -> rule2) OR ((((((triple7) -> rule4) triple6) -> rule1)) -> rule2))] Bob is cold.[(triple2)] Bob is furry.[(triple3 OR ((triple7) -> rule4))] Bob is green.[(triple4)] Bob is quiet.[(triple5 OR ((triple1 triple4) -> rule5) OR ((triple3 triple6) -> rule1) OR ((triple7 triple2) -> rule3) OR ((((triple3) -> rule6) triple2) -> rule3) OR ((((triple7) -> rule4) triple6) -> rule1))] Bob is round.[(triple6)] Bob is young.[(triple7 OR ((triple3) -> rule6))] Erin is blue.[(triple8 OR ((triple11) -> rule2) OR ((((triple12 triple9) -> rule3)) -> rule2))] Erin is cold.[(triple9)] Erin is green.[(triple10)] Erin is quiet.[(triple11 OR ((triple12 triple9) -> rule3))] Erin is young.[(triple12)] @1: Erin is furry.[(((triple12) -> rule4))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple5) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple3 triple6) -> (rule1 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple7 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple3) -> (rule6 % int3)) triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((((triple7) -> (rule4 % int3)) triple6) -> (rule1 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
((triple7) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((triple1 triple4) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple3 triple6) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple7 triple2) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple3) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple7) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple3) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple8
((triple11) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple12 triple9) -> (rule3 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple9
Erin is green.
("Erin" "is" "green" "+")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple11
((triple12 triple9) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple12
Erin is furry.
("Erin" "is" "furry" "+")
((triple12) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1