Bob is big. Bob is quiet. Bob is round. Bob is smart. Bob is white. Bob is young. Erin is big. Erin is quiet. Erin is red. Erin is round. Erin is smart. Erin is white. All smart, white things are young.
Bob is big.
("Bob" "is" "big" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
All smart, white things are young.
((("something" "is" "smart" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
Erin is red.
True
1
proof
[(triple9)]
("Erin" "is" "red" "+")
triple9
Erin is not round.
False
1
inv-proof
[(triple10)]
("Erin" "is" "round" "-")
triple10
Erin is young.
True
3
proof
[(((triple11 triple12) -> rule1))]
("Erin" "is" "young" "+")
((triple11 triple12) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not young.
False
3
inv-proof
[(((triple11 triple12) -> rule1))]
("Erin" "is" "young" "-")
((triple11 triple12) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
@0: Bob is big.[(triple1)] Bob is quiet.[(triple2)] Bob is round.[(triple3)] Bob is smart.[(triple4)] Bob is white.[(triple5)] Bob is young.[(triple6 OR ((triple4 triple5) -> rule1))] Erin is big.[(triple7)] Erin is quiet.[(triple8)] Erin is red.[(triple9)] Erin is round.[(triple10)] Erin is smart.[(triple11)] Erin is white.[(triple12)] @1: Erin is young.[(((triple11 triple12) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Bob is young.
("Bob" "is" "young" "+")
triple6
((triple4 triple5) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple7
Erin is quiet.
("Erin" "is" "quiet" "+")
triple8
Erin is red.
("Erin" "is" "red" "+")
triple9
Erin is round.
("Erin" "is" "round" "+")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
triple11
Erin is white.
("Erin" "is" "white" "+")
triple12
Erin is young.
("Erin" "is" "young" "+")
((triple11 triple12) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1