Anne is red. Anne is not round. Anne is not smart. Charlie is kind. Erin is big. Erin is kind. Erin is quiet. Gary is not big. Gary is quiet. Gary is red. Gary is rough. Kind things are round. All round things are big. If Anne is big and Anne is not red then Anne is not rough. If something is kind and smart then it is rough. If something is rough then it is quiet. All red things are quiet. Big, round things are smart. If something is quiet and not big then it is smart.
Anne is red.
("Anne" "is" "red" "+")
Anne is not round.
("Anne" "is" "round" "-")
Anne is not smart.
("Anne" "is" "smart" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is not big.
("Gary" "is" "big" "-")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
All round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If Anne is big and Anne is not red then Anne is not rough.
((("Anne" "is" "big" "+") ("Anne" "is" "red" "~")) -> ("Anne" "is" "rough" "-"))
If something is kind and smart then it is rough.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is rough then it is quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
All red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Big, round things are smart.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If something is quiet and not big then it is smart.
((("something" "is" "quiet" "+") ("something" "is" "big" "~")) -> ("something" "is" "smart" "+"))
Erin is quiet.
True
1
proof
[(triple7 OR ((((triple6 ((triple5 ((triple6) -> rule1)) -> rule7)) -> rule4)) -> rule5) OR ((((triple6 ((((((triple6) -> rule1)) -> rule2) ((triple6) -> rule1)) -> rule7)) -> rule4)) -> rule5))]
("Erin" "is" "quiet" "+")
triple7
((((triple6 ((triple5 ((triple6) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
((((triple6 ((((((triple6) -> (rule1 % int5))) -> (rule2 % int4)) ((triple6) -> (rule1 % int5))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
int5
Gary is not red.
False
1
inv-proof
[(triple10)]
("Gary" "is" "red" "-")
triple10
Erin is round.
True
2
proof
[(((triple6) -> rule1))]
("Erin" "is" "round" "+")
((triple6) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple4) -> rule1))]
("Charlie" "is" "round" "-")
((triple4) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
True
3
proof
[(((((triple4) -> rule1)) -> rule2))]
("Charlie" "is" "big" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is not big.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule2))]
("Charlie" "is" "big" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Erin is rough.
True
6
proof
[(((triple6 ((triple5 ((triple6) -> rule1)) -> rule7)) -> rule4) OR ((triple6 ((((((triple6) -> rule1)) -> rule2) ((triple6) -> rule1)) -> rule7)) -> rule4))]
("Erin" "is" "rough" "+")
((triple6 ((triple5 ((triple6) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((triple6 ((((((triple6) -> (rule1 % int4))) -> (rule2 % int3)) ((triple6) -> (rule1 % int4))) -> (rule7 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is not rough.
False
6
inv-proof
[(((triple6 ((triple5 ((triple6) -> rule1)) -> rule7)) -> rule4) OR ((triple6 ((((((triple6) -> rule1)) -> rule2) ((triple6) -> rule1)) -> rule7)) -> rule4))]
("Erin" "is" "rough" "-")
((triple6 ((triple5 ((triple6) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((triple6 ((((((triple6) -> (rule1 % int4))) -> (rule2 % int3)) ((triple6) -> (rule1 % int4))) -> (rule7 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Charlie is rough.
True
8
proof
[(((triple4 ((((((triple4) -> rule1)) -> rule2) ((triple4) -> rule1)) -> rule7)) -> rule4))]
("Charlie" "is" "rough" "+")
((triple4 ((((((triple4) -> (rule1 % int4))) -> (rule2 % int3)) ((triple4) -> (rule1 % int4))) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is not rough.
False
8
inv-proof
[(((triple4 ((((((triple4) -> rule1)) -> rule2) ((triple4) -> rule1)) -> rule7)) -> rule4))]
("Charlie" "is" "rough" "-")
((triple4 ((((((triple4) -> (rule1 % int4))) -> (rule2 % int3)) ((triple4) -> (rule1 % int4))) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is quiet.
True
9
proof
[(((((triple4 ((((((triple4) -> rule1)) -> rule2) ((triple4) -> rule1)) -> rule7)) -> rule4)) -> rule5))]
("Charlie" "is" "quiet" "+")
((((triple4 ((((((triple4) -> (rule1 % int5))) -> (rule2 % int4)) ((triple4) -> (rule1 % int5))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
int5
Charlie is not quiet.
False
9
inv-proof
[(((((triple4 ((((((triple4) -> rule1)) -> rule2) ((triple4) -> rule1)) -> rule7)) -> rule4)) -> rule5))]
("Charlie" "is" "quiet" "-")
((((triple4 ((((((triple4) -> (rule1 % int5))) -> (rule2 % int4)) ((triple4) -> (rule1 % int5))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
int5
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "round" "-")
Anne is big.
Unknown
rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "big" "+")
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "rough" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Anne is not round.[(triple2)] Anne is not smart.[(triple3)] Anne is red.[(triple1)] Charlie is kind.[(triple4)] Erin is big.[(triple5 OR ((((triple6) -> rule1)) -> rule2))] Erin is kind.[(triple6)] Erin is quiet.[(triple7 OR ((((triple6 ((triple5 ((triple6) -> rule1)) -> rule7)) -> rule4)) -> rule5) OR ((((triple6 ((((((triple6) -> rule1)) -> rule2) ((triple6) -> rule1)) -> rule7)) -> rule4)) -> rule5))] Gary is not big.[(triple8)] Gary is quiet.[(triple9 OR ((triple10) -> rule6) OR ((triple11) -> rule5))] Gary is red.[(triple10)] Gary is rough.[(triple11)] @1: Anne is quiet.[(((triple1) -> rule6))] Charlie is round.[(((triple4) -> rule1))] Erin is round.[(((triple6) -> rule1))] Gary is smart.[(((triple9 triple8) -> rule8) OR ((((triple10) -> rule6) triple8) -> rule8) OR ((((triple11) -> rule5) triple8) -> rule8))] @2: Charlie is big.[(((((triple4) -> rule1)) -> rule2))] Erin is smart.[(((triple5 ((triple6) -> rule1)) -> rule7) OR ((((((triple6) -> rule1)) -> rule2) ((triple6) -> rule1)) -> rule7))] @3: Charlie is smart.[(((((((triple4) -> rule1)) -> rule2) ((triple4) -> rule1)) -> rule7))] Erin is rough.[(((triple6 ((triple5 ((triple6) -> rule1)) -> rule7)) -> rule4) OR ((triple6 ((((((triple6) -> rule1)) -> rule2) ((triple6) -> rule1)) -> rule7)) -> rule4))] @4: Charlie is rough.[(((triple4 ((((((triple4) -> rule1)) -> rule2) ((triple4) -> rule1)) -> rule7)) -> rule4))] @5: Charlie is quiet.[(((((triple4 ((((((triple4) -> rule1)) -> rule2) ((triple4) -> rule1)) -> rule7)) -> rule4)) -> rule5))]
Anne is not round.
("Anne" "is" "round" "-")
triple2
Anne is not smart.
("Anne" "is" "smart" "-")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
((((triple6 ((triple5 ((triple6) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
((((triple6 ((((((triple6) -> (rule1 % int5))) -> (rule2 % int4)) ((triple6) -> (rule1 % int5))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
int5
Gary is not big.
("Gary" "is" "big" "-")
triple8
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
((triple10) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple11) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple10
Gary is rough.
("Gary" "is" "rough" "+")
triple11
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple4) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple6) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple9 triple8) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple10) -> (rule6 % int2)) triple8) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple11) -> (rule5 % int2)) triple8) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((triple5 ((triple6) -> (rule1 % int2))) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((((triple6) -> (rule1 % int3))) -> (rule2 % int2)) ((triple6) -> (rule1 % int3))) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2)) ((triple4) -> (rule1 % int3))) -> (rule7 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
((triple6 ((triple5 ((triple6) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((triple6 ((((((triple6) -> (rule1 % int4))) -> (rule2 % int3)) ((triple6) -> (rule1 % int4))) -> (rule7 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple4 ((((((triple4) -> (rule1 % int4))) -> (rule2 % int3)) ((triple4) -> (rule1 % int4))) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple4 ((((((triple4) -> (rule1 % int5))) -> (rule2 % int4)) ((triple4) -> (rule1 % int5))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
int5