Dave is big. Erin is smart. If something is furry then it is not blue. Nice things are not cold. Furry things are cold. White things are cold. If something is cold then it is not white. Smart things are furry.
Dave is big.
("Dave" "is" "big" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If something is furry then it is not blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "-"))
Nice things are not cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "-"))
Furry things are cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
White things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If something is cold then it is not white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "-"))
Smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Dave is big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
Erin is not smart.
False
1
inv-proof
[(triple2)]
("Erin" "is" "smart" "-")
triple2
Erin is furry.
True
2
proof
[(((triple2) -> rule6))]
("Erin" "is" "furry" "+")
((triple2) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple2) -> rule6))]
("Erin" "is" "furry" "-")
((triple2) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
True
3
proof
[(((((triple2) -> rule6)) -> rule3))]
("Erin" "is" "cold" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is blue.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule1))]
("Erin" "is" "blue" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is not white.
True
4
proof
[(((((((triple2) -> rule6)) -> rule3)) -> rule5))]
("Erin" "is" "white" "-")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is white.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule3)) -> rule5))]
("Erin" "is" "white" "+")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Dave is not cold.
Unknown
inv-rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "furry" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
@0: Dave is big.[(triple1)] Erin is smart.[(triple2)] @1: Erin is furry.[(((triple2) -> rule6))] @2: Erin is cold.[(((((triple2) -> rule6)) -> rule3))] Erin is not blue.[(((((triple2) -> rule6)) -> rule1))] @3: Erin is not white.[(((((((triple2) -> rule6)) -> rule3)) -> rule5))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
((triple2) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is not blue.
("Erin" "is" "blue" "-")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is not white.
("Erin" "is" "white" "-")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3