Bob is furry. Bob is kind. Charlie is nice. Dave is furry. Erin is cold. Erin is not furry. Erin is red. If someone is nice and not furry then they are kind. Nice people are cold. If someone is furry then they are cold. If someone is big and furry then they are cold. If Bob is kind and Bob is blue then Bob is cold. All nice people are blue. Blue people are nice. If Bob is cold then Bob is blue.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is not furry.
("Erin" "is" "furry" "-")
Erin is red.
("Erin" "is" "red" "+")
If someone is nice and not furry then they are kind.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "kind" "+"))
Nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone is furry then they are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
If someone is big and furry then they are cold.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
If Bob is kind and Bob is blue then Bob is cold.
((("Bob" "is" "kind" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "cold" "+"))
All nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If Bob is cold then Bob is blue.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "blue" "+"))
Erin is cold.
True
1
proof
[(triple5)]
("Erin" "is" "cold" "+")
triple5
Erin is not red.
False
1
inv-proof
[(triple7)]
("Erin" "is" "red" "-")
triple7
Charlie is blue.
True
2
proof
[(((triple3) -> rule6))]
("Charlie" "is" "blue" "+")
((triple3) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple3) -> rule2))]
("Charlie" "is" "cold" "-")
((triple3) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Bob is blue.
True
3
proof
[(((((triple1) -> rule3)) -> rule8))]
("Bob" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not blue.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule8))]
("Bob" "is" "blue" "-")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "kind" "-")
Dave is nice.
Unknown
rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("Dave" "is" "nice" "+")
Erin is not blue.
Unknown
inv-rconc
[@2: Erin is blue.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Erin" "is" "blue" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is furry.[(triple1)] Bob is kind.[(triple2)] Charlie is nice.[(triple3)] Dave is furry.[(triple4)] Erin is cold.[(triple5)] Erin is not furry.[(triple6)] Erin is red.[(triple7)] @1: Bob is cold.[(((triple1) -> rule3))] Charlie is blue.[(((triple3) -> rule6))] Charlie is cold.[(((triple3) -> rule2))] Dave is cold.[(((triple4) -> rule3))] @2: Bob is blue.[(((((triple1) -> rule3)) -> rule8))] @3: Bob is nice.[(((((((triple1) -> rule3)) -> rule8)) -> rule7))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is not furry.
("Erin" "is" "furry" "-")
triple6
Erin is red.
("Erin" "is" "red" "+")
triple7
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple3) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple4) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3