Charlie is big. Charlie is blue. Charlie is not quiet. Charlie is rough. Charlie is not round. Erin is not big. Erin is quiet. If something is rough and not round then it is big. If Charlie is not furry and Charlie is not big then Charlie is not red.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
Erin is not big.
("Erin" "is" "big" "-")
Erin is quiet.
("Erin" "is" "quiet" "+")
If something is rough and not round then it is big.
((("something" "is" "rough" "+") ("something" "is" "round" "~")) -> ("something" "is" "big" "+"))
If Charlie is not furry and Charlie is not big then Charlie is not red.
((("Charlie" "is" "furry" "~") ("Charlie" "is" "big" "~")) -> ("Charlie" "is" "red" "-"))
Charlie is blue.
True
1
proof
[(triple2)]
("Charlie" "is" "blue" "+")
triple2
Erin is big.
False
1
inv-proof
[(triple6)]
("Erin" "is" "big" "+")
triple6
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Charlie is big.[(triple1 OR ((triple4 triple5) -> rule1))] Charlie is blue.[(triple2)] Charlie is not quiet.[(triple3)] Charlie is not round.[(triple5)] Charlie is rough.[(triple4)] Erin is not big.[(triple6)] Erin is quiet.[(triple7)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple4 triple5) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple3
Charlie is not round.
("Charlie" "is" "round" "-")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Erin is not big.
("Erin" "is" "big" "-")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7