Anne is not furry. Anne is round. Charlie is round. Erin is cold. Erin is furry. Harry is furry. Harry is quiet. Cold people are not big. Nice people are quiet. All quiet, round people are cold. All round people are nice. All quiet, round people are nice. If someone is round and not big then they are rough. If someone is furry and not round then they are rough.
Anne is not furry.
("Anne" "is" "furry" "-")
Anne is round.
("Anne" "is" "round" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Cold people are not big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "-"))
Nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
All quiet, round people are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
All round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
All quiet, round people are nice.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If someone is round and not big then they are rough.
((("someone" "is" "round" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "rough" "+"))
If someone is furry and not round then they are rough.
((("someone" "is" "furry" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "rough" "+"))
Anne is round.
True
1
proof
[(triple2)]
("Anne" "is" "round" "+")
triple2
Anne is not round.
False
1
inv-proof
[(triple2)]
("Anne" "is" "round" "-")
triple2
Anne is nice.
True
2
proof
[(((triple2) -> rule4))]
("Anne" "is" "nice" "+")
((triple2) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple3) -> rule4))]
("Charlie" "is" "nice" "-")
((triple3) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
True
3
proof
[(((((triple3) -> rule4)) -> rule2))]
("Charlie" "is" "quiet" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Anne is not quiet.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule2))]
("Anne" "is" "quiet" "-")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Charlie is cold.
True
5
proof
[(((((((triple3) -> rule4)) -> rule2) triple3) -> rule3))]
("Charlie" "is" "cold" "+")
((((((triple3) -> (rule4 % int3))) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not cold.
False
5
inv-proof
[(((((((triple3) -> rule4)) -> rule2) triple3) -> rule3))]
("Charlie" "is" "cold" "-")
((((((triple3) -> (rule4 % int3))) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not big.
True
6
proof
[(((((((((triple3) -> rule4)) -> rule2) triple3) -> rule3)) -> rule1))]
("Charlie" "is" "big" "-")
((((((((triple3) -> (rule4 % int4))) -> (rule2 % int3)) triple3) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Anne is big.
False
6
inv-proof
[(((((((((triple2) -> rule4)) -> rule2) triple2) -> rule3)) -> rule1))]
("Anne" "is" "big" "+")
((((((((triple2) -> (rule4 % int4))) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is rough.
True
8
proof
[(((triple2 ((((((((triple2) -> rule4)) -> rule2) triple2) -> rule3)) -> rule1)) -> rule6))]
("Anne" "is" "rough" "+")
((triple2 ((((((((triple2) -> (rule4 % int5))) -> (rule2 % int4)) triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not big.
("Anne" "is" "big" "-")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
int5
Anne is not rough.
False
8
inv-proof
[(((triple2 ((((((((triple2) -> rule4)) -> rule2) triple2) -> rule3)) -> rule1)) -> rule6))]
("Anne" "is" "rough" "-")
((triple2 ((((((((triple2) -> (rule4 % int5))) -> (rule2 % int4)) triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not big.
("Anne" "is" "big" "-")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
int5
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "rough" "-")
Harry is rough.
Unknown
rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "rough" "+")
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is quiet.
Unknown
rconc
[@2: Erin is quiet.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Erin" "is" "quiet" "+")
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "nice" "-")
Harry is cold.
Unknown
rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "cold" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Anne is not furry.[(triple1)] Anne is round.[(triple2)] Charlie is round.[(triple3)] Erin is cold.[(triple4)] Erin is furry.[(triple5)] Harry is furry.[(triple6)] Harry is quiet.[(triple7)] @1: Anne is nice.[(((triple2) -> rule4))] Charlie is nice.[(((triple3) -> rule4))] Erin is not big.[(((triple4) -> rule1))] @2: Anne is quiet.[(((((triple2) -> rule4)) -> rule2))] Charlie is quiet.[(((((triple3) -> rule4)) -> rule2))] @3: Anne is cold.[(((((((triple2) -> rule4)) -> rule2) triple2) -> rule3))] Charlie is cold.[(((((((triple3) -> rule4)) -> rule2) triple3) -> rule3))] @4: Anne is not big.[(((((((((triple2) -> rule4)) -> rule2) triple2) -> rule3)) -> rule1))] Charlie is not big.[(((((((((triple3) -> rule4)) -> rule2) triple3) -> rule3)) -> rule1))] @5: Anne is rough.[(((triple2 ((((((((triple2) -> rule4)) -> rule2) triple2) -> rule3)) -> rule1)) -> rule6))] Charlie is rough.[(((triple3 ((((((((triple3) -> rule4)) -> rule2) triple3) -> rule3)) -> rule1)) -> rule6))]
Anne is not furry.
("Anne" "is" "furry" "-")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
Erin is furry.
("Erin" "is" "furry" "+")
triple5
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Anne is nice.
("Anne" "is" "nice" "+")
((triple2) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple3) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Erin is not big.
("Erin" "is" "big" "-")
((triple4) -> (rule1 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple3) -> (rule4 % int3))) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Anne is not big.
("Anne" "is" "big" "-")
((((((((triple2) -> (rule4 % int4))) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Charlie is not big.
("Charlie" "is" "big" "-")
((((((((triple3) -> (rule4 % int4))) -> (rule2 % int3)) triple3) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
((triple2 ((((((((triple2) -> (rule4 % int5))) -> (rule2 % int4)) triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not big.
("Anne" "is" "big" "-")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
int5
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple3 ((((((((triple3) -> (rule4 % int5))) -> (rule2 % int4)) triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not big.
("Charlie" "is" "big" "-")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
int5