Bob is big. Bob is green. Bob is kind. Bob is quiet. Bob is red. Bob is white. Bob is young. Erin is big. Erin is kind. Erin is quiet. Erin is red. Erin is white. All red things are white. All green things are big. If something is quiet then it is young. All green things are young. If Erin is young and Erin is white then Erin is big. If Bob is red and Bob is green then Bob is kind. If something is red and green then it is white. If something is young and kind then it is green.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is white.
("Erin" "is" "white" "+")
All red things are white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
All green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is quiet then it is young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
All green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If Erin is young and Erin is white then Erin is big.
((("Erin" "is" "young" "+") ("Erin" "is" "white" "+")) -> ("Erin" "is" "big" "+"))
If Bob is red and Bob is green then Bob is kind.
((("Bob" "is" "red" "+") ("Bob" "is" "green" "+")) -> ("Bob" "is" "kind" "+"))
If something is red and green then it is white.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is young and kind then it is green.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Bob is young.
True
1
proof
[(triple7 OR ((triple2) -> rule4) OR ((triple4) -> rule3))]
("Bob" "is" "young" "+")
triple7
((triple2) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple4) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Erin is not red.
False
1
inv-proof
[(triple11)]
("Erin" "is" "red" "-")
triple11
Erin is young.
True
2
proof
[(((triple10) -> rule3))]
("Erin" "is" "young" "+")
((triple10) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not young.
False
2
inv-proof
[(((triple10) -> rule3))]
("Erin" "is" "young" "-")
((triple10) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is green.
True
4
proof
[(((((triple10) -> rule3) triple9) -> rule8))]
("Erin" "is" "green" "+")
((((triple10) -> (rule3 % int2)) triple9) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not green.
False
4
inv-proof
[(((((triple10) -> rule3) triple9) -> rule8))]
("Erin" "is" "green" "-")
((((triple10) -> (rule3 % int2)) triple9) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
@0: Bob is big.[(triple1 OR ((triple2) -> rule2) OR ((((triple7 triple3) -> rule8)) -> rule2) OR ((((((triple4) -> rule3) triple3) -> rule8)) -> rule2))] Bob is green.[(triple2 OR ((triple7 triple3) -> rule8) OR ((((triple4) -> rule3) triple3) -> rule8))] Bob is kind.[(triple3 OR ((triple5 triple2) -> rule6))] Bob is quiet.[(triple4)] Bob is red.[(triple5)] Bob is white.[(triple6 OR ((triple5) -> rule1) OR ((triple5 triple2) -> rule7) OR ((triple5 ((triple7 triple3) -> rule8)) -> rule7) OR ((triple5 ((((triple4) -> rule3) triple3) -> rule8)) -> rule7))] Bob is young.[(triple7 OR ((triple2) -> rule4) OR ((triple4) -> rule3))] Erin is big.[(triple8 OR ((((triple10) -> rule3) triple12) -> rule5) OR ((((triple10) -> rule3) ((triple11) -> rule1)) -> rule5) OR ((((((triple10) -> rule3) triple9) -> rule8)) -> rule2) OR ((((triple10) -> rule3) ((triple11 ((((triple10) -> rule3) triple9) -> rule8)) -> rule7)) -> rule5))] Erin is kind.[(triple9)] Erin is quiet.[(triple10)] Erin is red.[(triple11)] Erin is white.[(triple12 OR ((triple11) -> rule1) OR ((triple11 ((((triple10) -> rule3) triple9) -> rule8)) -> rule7))] @1: Erin is young.[(((triple10) -> rule3))] @2: Erin is green.[(((((triple10) -> rule3) triple9) -> rule8))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple2) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple7 triple3) -> (rule8 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((((triple4) -> (rule3 % int3)) triple3) -> (rule8 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
triple2
((triple7 triple3) -> (rule8 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple4) -> (rule3 % int2)) triple3) -> (rule8 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple5 triple2) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
((triple5) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple5 triple2) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple5 ((triple7 triple3) -> (rule8 % int2))) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((triple5 ((((triple4) -> (rule3 % int3)) triple3) -> (rule8 % int2))) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple2) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple4) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple8
((((triple10) -> (rule3 % int2)) triple12) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((triple10) -> (rule3 % int3)) ((triple11) -> (rule1 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((((((triple10) -> (rule3 % int3)) triple9) -> (rule8 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((((triple10) -> (rule3 % int4)) ((triple11 ((((triple10) -> (rule3 % int4)) triple9) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
triple9
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
Erin is red.
("Erin" "is" "red" "+")
triple11
Erin is white.
("Erin" "is" "white" "+")
triple12
((triple11) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple11 ((((triple10) -> (rule3 % int3)) triple9) -> (rule8 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
((triple10) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((((triple10) -> (rule3 % int2)) triple9) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2