Anne is round. Erin is rough. Erin is smart. If Anne is round and Anne is big then Anne is quiet. All round things are big. If Anne is rough and Anne is big then Anne is round. If Erin is white and Erin is rough then Erin is big. If Anne is round then Anne is young. Young, big things are quiet. If something is quiet then it is rough. If something is white then it is round.
Anne is round.
("Anne" "is" "round" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If Anne is round and Anne is big then Anne is quiet.
((("Anne" "is" "round" "+") ("Anne" "is" "big" "+")) -> ("Anne" "is" "quiet" "+"))
All round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If Anne is rough and Anne is big then Anne is round.
((("Anne" "is" "rough" "+") ("Anne" "is" "big" "+")) -> ("Anne" "is" "round" "+"))
If Erin is white and Erin is rough then Erin is big.
((("Erin" "is" "white" "+") ("Erin" "is" "rough" "+")) -> ("Erin" "is" "big" "+"))
If Anne is round then Anne is young.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "young" "+"))
Young, big things are quiet.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet then it is rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is white then it is round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Erin is rough.
True
1
proof
[(triple2)]
("Erin" "is" "rough" "+")
triple2
Anne is not round.
False
1
inv-proof
[(triple1)]
("Anne" "is" "round" "-")
triple1
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Anne is round.[(triple1)] Erin is rough.[(triple2)] Erin is smart.[(triple3)] @1: Anne is big.[(((triple1) -> rule2))] Anne is young.[(((triple1) -> rule5))] @2: Anne is quiet.[(((triple1 ((triple1) -> rule2)) -> rule1) OR ((((triple1) -> rule5) ((triple1) -> rule2)) -> rule6))] @3: Anne is rough.[(((((triple1 ((triple1) -> rule2)) -> rule1)) -> rule7) OR ((((((triple1) -> rule5) ((triple1) -> rule2)) -> rule6)) -> rule7))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple1) -> (rule5 % int3)) ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
((((((triple1) -> (rule5 % int4)) ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4