Dave is furry. Dave is nice. Erin is cold. If Erin is round then Erin is nice. If something is quiet then it is furry. All quiet, big things are round. If Dave is nice and Dave is cold then Dave is big. If something is big and cold then it is blue. All cold things are furry. If something is round then it is big. All cold things are round.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Erin is cold.
("Erin" "is" "cold" "+")
If Erin is round then Erin is nice.
((("Erin" "is" "round" "+")) -> ("Erin" "is" "nice" "+"))
If something is quiet then it is furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
All quiet, big things are round.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If Dave is nice and Dave is cold then Dave is big.
((("Dave" "is" "nice" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "big" "+"))
If something is big and cold then it is blue.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
All cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
If something is round then it is big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All cold things are round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Erin is cold.
True
1
proof
[(triple3)]
("Erin" "is" "cold" "+")
triple3
Dave is not furry.
False
1
inv-proof
[(triple1)]
("Dave" "is" "furry" "-")
triple1
Erin is furry.
True
2
proof
[(((triple3) -> rule6))]
("Erin" "is" "furry" "+")
((triple3) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple3) -> rule6))]
("Erin" "is" "furry" "-")
((triple3) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is nice.
True
3
proof
[(((((triple3) -> rule8)) -> rule1))]
("Erin" "is" "nice" "+")
((((triple3) -> (rule8 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not nice.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule1))]
("Erin" "is" "nice" "-")
((((triple3) -> (rule8 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is big.
Unknown
rconc
[@2: Dave is big.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Dave" "is" "big" "+")
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Dave is furry.[(triple1)] Dave is nice.[(triple2)] Erin is cold.[(triple3)] @1: Erin is furry.[(((triple3) -> rule6))] Erin is round.[(((triple3) -> rule8))] @2: Erin is big.[(((((triple3) -> rule8)) -> rule7))] Erin is nice.[(((((triple3) -> rule8)) -> rule1))] @3: Erin is blue.[(((((((triple3) -> rule8)) -> rule7) triple3) -> rule5))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
((triple3) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple3) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple3) -> (rule8 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((((((triple3) -> (rule8 % int3))) -> (rule7 % int2)) triple3) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3