Anne is not furry. Charlie is furry. Dave is nice. Erin is round. If Erin is rough then Erin is smart. If someone is cold and furry then they are round. All furry people are not round. If someone is round and quiet then they are cold. Cold, rough people are not furry. If Dave is nice then Dave is cold. If someone is nice then they are quiet. All round people are nice.
Anne is not furry.
("Anne" "is" "furry" "-")
Charlie is furry.
("Charlie" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Erin is round.
("Erin" "is" "round" "+")
If Erin is rough then Erin is smart.
((("Erin" "is" "rough" "+")) -> ("Erin" "is" "smart" "+"))
If someone is cold and furry then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
All furry people are not round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "-"))
If someone is round and quiet then they are cold.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
Cold, rough people are not furry.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "-"))
If Dave is nice then Dave is cold.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "cold" "+"))
If someone is nice then they are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
All round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
Anne is not furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Dave is not nice.
False
1
inv-proof
[(triple3)]
("Dave" "is" "nice" "-")
triple3
Dave is quiet.
True
2
proof
[(((triple3) -> rule7))]
("Dave" "is" "quiet" "+")
((triple3) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Charlie is round.
False
2
inv-proof
[(((triple2) -> rule3))]
("Charlie" "is" "round" "+")
((triple2) -> (rule3 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Erin is quiet.
True
3
proof
[(((((triple4) -> rule8)) -> rule7))]
("Erin" "is" "quiet" "+")
((((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not quiet.
False
3
inv-proof
[(((((triple4) -> rule8)) -> rule7))]
("Erin" "is" "quiet" "-")
((((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is cold.
True
5
proof
[(((triple4 ((((triple4) -> rule8)) -> rule7)) -> rule4))]
("Erin" "is" "cold" "+")
((triple4 ((((triple4) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is not cold.
False
5
inv-proof
[(((triple4 ((((triple4) -> rule8)) -> rule7)) -> rule4))]
("Erin" "is" "cold" "-")
((triple4 ((((triple4) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Charlie is not quiet.
Unknown
inv-rconc
[@2: Charlie is quiet.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "cold" "-")
Dave is round.
Unknown
rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "round" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is not furry.[(triple1)] Charlie is furry.[(triple2)] Dave is nice.[(triple3)] Erin is round.[(triple4)] @1: Charlie is not round.[(((triple2) -> rule3))] Dave is cold.[(((triple3) -> rule6))] Dave is quiet.[(((triple3) -> rule7))] Erin is nice.[(((triple4) -> rule8))] @2: Erin is quiet.[(((((triple4) -> rule8)) -> rule7))] @3: Erin is cold.[(((triple4 ((((triple4) -> rule8)) -> rule7)) -> rule4))]
Anne is not furry.
("Anne" "is" "furry" "-")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Erin is round.
("Erin" "is" "round" "+")
triple4
Charlie is not round.
("Charlie" "is" "round" "-")
((triple2) -> (rule3 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple3) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple3) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple4) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((triple4 ((((triple4) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3