Bob is big. Bob is cold. Bob is nice. Bob is quiet. Bob is rough. Bob is white. Bob is young. Erin is big. Erin is cold. Erin is nice. Erin is quiet. Erin is rough. Erin is white. Erin is young. White, cold things are big. Cold, young things are quiet. All cold things are young.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
White, cold things are big.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Cold, young things are quiet.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
All cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
Bob is rough.
True
1
proof
[(triple5)]
("Bob" "is" "rough" "+")
triple5
Erin is not young.
False
1
inv-proof
[(triple14 OR ((triple9) -> rule3))]
("Erin" "is" "young" "-")
triple14
((triple9) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
@0: Bob is big.[(triple1 OR ((triple6 triple2) -> rule1))] Bob is cold.[(triple2)] Bob is nice.[(triple3)] Bob is quiet.[(triple4 OR ((triple2 triple7) -> rule2) OR ((triple2 ((triple2) -> rule3)) -> rule2))] Bob is rough.[(triple5)] Bob is white.[(triple6)] Bob is young.[(triple7 OR ((triple2) -> rule3))] Erin is big.[(triple8 OR ((triple13 triple9) -> rule1))] Erin is cold.[(triple9)] Erin is nice.[(triple10)] Erin is quiet.[(triple11 OR ((triple9 triple14) -> rule2) OR ((triple9 ((triple9) -> rule3)) -> rule2))] Erin is rough.[(triple12)] Erin is white.[(triple13)] Erin is young.[(triple14 OR ((triple9) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple6 triple2) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple2 triple7) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple2) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple8
((triple13 triple9) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple9
Erin is nice.
("Erin" "is" "nice" "+")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple11
((triple9 triple14) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple9 ((triple9) -> (rule3 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple12
Erin is white.
("Erin" "is" "white" "+")
triple13
Erin is young.
("Erin" "is" "young" "+")
triple14
((triple9) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1