Erin is big. Erin is green. Erin is kind. Erin is red. Erin is rough. Erin is round. Erin is smart. If something is smart and rough then it is kind.
Erin is big.
("Erin" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If something is smart and rough then it is kind.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Erin is green.
True
1
proof
[(triple2)]
("Erin" "is" "green" "+")
triple2
Erin is not kind.
False
1
inv-proof
[(triple3 OR ((triple7 triple5) -> rule1))]
("Erin" "is" "kind" "-")
triple3
((triple7 triple5) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
@0: Erin is big.[(triple1)] Erin is green.[(triple2)] Erin is kind.[(triple3 OR ((triple7 triple5) -> rule1))] Erin is red.[(triple4)] Erin is rough.[(triple5)] Erin is round.[(triple6)] Erin is smart.[(triple7)]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
((triple7 triple5) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple4
Erin is rough.
("Erin" "is" "rough" "+")
triple5
Erin is round.
("Erin" "is" "round" "+")
triple6
Erin is smart.
("Erin" "is" "smart" "+")
triple7