Bob is not furry. Bob is kind. Bob is rough. Bob is white. Charlie is cold. Charlie is furry. Charlie is red. Erin is cold. Erin is furry. Erin is kind. Erin is red. Erin is rough. Erin is white. Harry is not kind. Harry is rough. If Bob is big then Bob is kind. If Harry is not rough then Harry is red. Furry, kind people are white. If someone is rough and not kind then they are red. Kind, cold people are red. All rough, red people are cold.
Bob is not furry.
("Bob" "is" "furry" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is rough.
("Harry" "is" "rough" "+")
If Bob is big then Bob is kind.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "kind" "+"))
If Harry is not rough then Harry is red.
((("Harry" "is" "rough" "~")) -> ("Harry" "is" "red" "+"))
Furry, kind people are white.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
If someone is rough and not kind then they are red.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "red" "+"))
Kind, cold people are red.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
All rough, red people are cold.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Bob is kind.
True
1
proof
[(triple2)]
("Bob" "is" "kind" "+")
triple2
Harry is kind.
False
1
inv-proof
[(triple14)]
("Harry" "is" "kind" "+")
triple14
Harry is red.
True
3
proof
[(((triple15 triple14) -> rule4))]
("Harry" "is" "red" "+")
((triple15 triple14) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not red.
False
3
inv-proof
[(((triple15 triple14) -> rule4))]
("Harry" "is" "red" "-")
((triple15 triple14) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
True
5
proof
[(((triple15 ((triple15 triple14) -> rule4)) -> rule6))]
("Harry" "is" "cold" "+")
((triple15 ((triple15 triple14) -> (rule4 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not cold.
False
5
inv-proof
[(((triple15 ((triple15 triple14) -> rule4)) -> rule6))]
("Harry" "is" "cold" "-")
((triple15 ((triple15 triple14) -> (rule4 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Bob is not cold.
Unknown
inv-rconc
[@2: Bob is cold.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Bob" "is" "cold" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "white" "+")
Bob is not red.
Unknown
inv-rconc
[@3: Bob is red.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule4 <- FAIL)]]
("Bob" "is" "red" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is kind.[(triple2)] Bob is not furry.[(triple1)] Bob is rough.[(triple3)] Bob is white.[(triple4)] Charlie is cold.[(triple5)] Charlie is furry.[(triple6)] Charlie is red.[(triple7)] Erin is cold.[(triple8 OR ((triple12 triple11) -> rule6))] Erin is furry.[(triple9)] Erin is kind.[(triple10)] Erin is red.[(triple11 OR ((triple10 triple8) -> rule5))] Erin is rough.[(triple12)] Erin is white.[(triple13 OR ((triple9 triple10) -> rule3))] Harry is not kind.[(triple14)] Harry is rough.[(triple15)] @1: Harry is red.[(((triple15 triple14) -> rule4))] @2: Harry is cold.[(((triple15 ((triple15 triple14) -> rule4)) -> rule6))]
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is not furry.
("Bob" "is" "furry" "-")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Charlie is red.
("Charlie" "is" "red" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
triple8
((triple12 triple11) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple9
Erin is kind.
("Erin" "is" "kind" "+")
triple10
Erin is red.
("Erin" "is" "red" "+")
triple11
((triple10 triple8) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple12
Erin is white.
("Erin" "is" "white" "+")
triple13
((triple9 triple10) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Harry is not kind.
("Harry" "is" "kind" "-")
triple14
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Harry is red.
("Harry" "is" "red" "+")
((triple15 triple14) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple15 ((triple15 triple14) -> (rule4 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2