Erin is big. Erin is kind. Erin is quiet. Red things are blue. Kind things are quiet. If Erin is big and Erin is rough then Erin is quiet. Blue things are quiet. Furry, red things are quiet. If something is kind then it is big. If something is rough and red then it is furry. If Erin is quiet then Erin is big.
Erin is big.
("Erin" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Kind things are quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If Erin is big and Erin is rough then Erin is quiet.
((("Erin" "is" "big" "+") ("Erin" "is" "rough" "+")) -> ("Erin" "is" "quiet" "+"))
Blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
Furry, red things are quiet.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If something is kind then it is big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
If something is rough and red then it is furry.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If Erin is quiet then Erin is big.
((("Erin" "is" "quiet" "+")) -> ("Erin" "is" "big" "+"))
Erin is big.
True
1
proof
[(triple1 OR ((triple2) -> rule6) OR ((triple3) -> rule8) OR ((((triple2) -> rule2)) -> rule8))]
("Erin" "is" "big" "+")
triple1
((triple2) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple3) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is not big.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule6) OR ((triple3) -> rule8) OR ((((triple2) -> rule2)) -> rule8))]
("Erin" "is" "big" "-")
triple1
((triple2) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple3) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "blue" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Erin is big.[(triple1 OR ((triple2) -> rule6) OR ((triple3) -> rule8) OR ((((triple2) -> rule2)) -> rule8))] Erin is kind.[(triple2)] Erin is quiet.[(triple3 OR ((triple2) -> rule2))]
Erin is big.
("Erin" "is" "big" "+")
triple1
((triple2) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple3) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
((triple2) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1