Anne is rough. Dave is rough. Erin is quiet. Rough people are cold. All round people are quiet. All furry people are quiet. If someone is furry and big then they are round. All cold, rough people are quiet. If Erin is big and Erin is round then Erin is green. Cold people are big. Quiet, big people are green.
Anne is rough.
("Anne" "is" "rough" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
All round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
All furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If someone is furry and big then they are round.
((("someone" "is" "furry" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
All cold, rough people are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If Erin is big and Erin is round then Erin is green.
((("Erin" "is" "big" "+") ("Erin" "is" "round" "+")) -> ("Erin" "is" "green" "+"))
Cold people are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
Quiet, big people are green.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Dave is rough.
True
1
proof
[(triple2)]
("Dave" "is" "rough" "+")
triple2
Dave is not rough.
False
1
inv-proof
[(triple2)]
("Dave" "is" "rough" "-")
triple2
Dave is cold.
True
2
proof
[(((triple2) -> rule1))]
("Dave" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Anne is not cold.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "cold" "-")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Dave is big.
True
3
proof
[(((((triple2) -> rule1)) -> rule7))]
("Dave" "is" "big" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Anne is not quiet.
False
4
inv-proof
[(((((triple1) -> rule1) triple1) -> rule5))]
("Anne" "is" "quiet" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is round.
Unknown
rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "round" "+")
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "round" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Anne is rough.[(triple1)] Dave is rough.[(triple2)] Erin is quiet.[(triple3)] @1: Anne is cold.[(((triple1) -> rule1))] Dave is cold.[(((triple2) -> rule1))] @2: Anne is big.[(((((triple1) -> rule1)) -> rule7))] Anne is quiet.[(((((triple1) -> rule1) triple1) -> rule5))] Dave is big.[(((((triple2) -> rule1)) -> rule7))] Dave is quiet.[(((((triple2) -> rule1) triple2) -> rule5))] @3: Anne is green.[(((((((triple1) -> rule1) triple1) -> rule5) ((((triple1) -> rule1)) -> rule7)) -> rule8))] Dave is green.[(((((((triple2) -> rule1) triple2) -> rule5) ((((triple2) -> rule1)) -> rule7)) -> rule8))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((((((triple1) -> (rule1 % int4)) triple1) -> (rule5 % int3)) ((((triple1) -> (rule1 % int4))) -> (rule7 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
((((((triple2) -> (rule1 % int4)) triple2) -> (rule5 % int3)) ((((triple2) -> (rule1 % int4))) -> (rule7 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4