Bob is big. Dave is furry. Erin is white. Harry is kind. If Bob is red and Bob is furry then Bob is nice. All red, white things are cold. All nice, cold things are furry. Cold things are nice. Kind things are cold. Red things are big.
Bob is big.
("Bob" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If Bob is red and Bob is furry then Bob is nice.
((("Bob" "is" "red" "+") ("Bob" "is" "furry" "+")) -> ("Bob" "is" "nice" "+"))
All red, white things are cold.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
All nice, cold things are furry.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
Cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
Red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Erin is white.
True
1
proof
[(triple3)]
("Erin" "is" "white" "+")
triple3
Erin is not white.
False
1
inv-proof
[(triple3)]
("Erin" "is" "white" "-")
triple3
Harry is cold.
True
2
proof
[(((triple4) -> rule5))]
("Harry" "is" "cold" "+")
((triple4) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple4) -> rule5))]
("Harry" "is" "cold" "-")
((triple4) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
True
3
proof
[(((((triple4) -> rule5)) -> rule4))]
("Harry" "is" "nice" "+")
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not nice.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule4))]
("Harry" "is" "nice" "-")
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is furry.
True
6
proof
[(((((((triple4) -> rule5)) -> rule4) ((triple4) -> rule5)) -> rule3))]
("Harry" "is" "furry" "+")
((((((triple4) -> (rule5 % int3))) -> (rule4 % int2)) ((triple4) -> (rule5 % int3))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not furry.
False
6
inv-proof
[(((((((triple4) -> rule5)) -> rule4) ((triple4) -> rule5)) -> rule3))]
("Harry" "is" "furry" "-")
((((((triple4) -> (rule5 % int3))) -> (rule4 % int2)) ((triple4) -> (rule5 % int3))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Bob is not furry.
Unknown
inv-rconc
[@2: Bob is furry.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Bob" "is" "furry" "-")
Erin is nice.
Unknown
rconc
[@2: Erin is nice.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Erin" "is" "nice" "+")
Bob is not nice.
Unknown
inv-rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Bob" "is" "nice" "-")
Erin is cold.
Unknown
rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "cold" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Bob is big.[(triple1)] Dave is furry.[(triple2)] Erin is white.[(triple3)] Harry is kind.[(triple4)] @1: Harry is cold.[(((triple4) -> rule5))] @2: Harry is nice.[(((((triple4) -> rule5)) -> rule4))] @3: Harry is furry.[(((((((triple4) -> rule5)) -> rule4) ((triple4) -> rule5)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
((triple4) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((((triple4) -> (rule5 % int3))) -> (rule4 % int2)) ((triple4) -> (rule5 % int3))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3