Erin is big. Erin is green. Erin is kind. Erin is quiet. Erin is round. Erin is smart. Erin is young. Gary is big. Gary is green. Gary is kind. Gary is quiet. Gary is round. Gary is smart. Gary is young. If something is young and smart then it is round. If something is round and young then it is green.
Erin is big.
("Erin" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is young and smart then it is round.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
If something is round and young then it is green.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
Erin is big.
True
1
proof
[(triple1)]
("Erin" "is" "big" "+")
triple1
Erin is not quiet.
False
1
inv-proof
[(triple4)]
("Erin" "is" "quiet" "-")
triple4
@0: Erin is big.[(triple1)] Erin is green.[(triple2 OR ((triple5 triple7) -> rule2) OR ((((triple7 triple6) -> rule1) triple7) -> rule2))] Erin is kind.[(triple3)] Erin is quiet.[(triple4)] Erin is round.[(triple5 OR ((triple7 triple6) -> rule1))] Erin is smart.[(triple6)] Erin is young.[(triple7)] Gary is big.[(triple8)] Gary is green.[(triple9 OR ((triple12 triple14) -> rule2) OR ((((triple14 triple13) -> rule1) triple14) -> rule2))] Gary is kind.[(triple10)] Gary is quiet.[(triple11)] Gary is round.[(triple12 OR ((triple14 triple13) -> rule1))] Gary is smart.[(triple13)] Gary is young.[(triple14)]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
((triple5 triple7) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple7 triple6) -> (rule1 % int2)) triple7) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple5
((triple7 triple6) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is green.
("Gary" "is" "green" "+")
triple9
((triple12 triple14) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple14 triple13) -> (rule1 % int2)) triple14) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple10
Gary is quiet.
("Gary" "is" "quiet" "+")
triple11
Gary is round.
("Gary" "is" "round" "+")
triple12
((triple14 triple13) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple13
Gary is young.
("Gary" "is" "young" "+")
triple14