Dave is cold. Dave is not furry. Dave is green. Dave is rough. Erin is big. Erin is not cold. Erin is furry. Erin is green. Erin is not nice. Erin is not rough. Erin is white. Gary is big. Gary is not cold. Gary is green. Gary is nice. Gary is not rough. All nice, furry people are cold. If someone is nice and not big then they are furry. If someone is rough and white then they are nice. Green people are white. All rough people are white. Rough, furry people are white.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is not nice.
("Erin" "is" "nice" "-")
Erin is not rough.
("Erin" "is" "rough" "-")
Erin is white.
("Erin" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
All nice, furry people are cold.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice and not big then they are furry.
((("someone" "is" "nice" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "furry" "+"))
If someone is rough and white then they are nice.
((("someone" "is" "rough" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
Green people are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
All rough people are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
Rough, furry people are white.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
Gary is nice.
True
1
proof
[(triple15)]
("Gary" "is" "nice" "+")
triple15
Gary is rough.
False
1
inv-proof
[(triple16)]
("Gary" "is" "rough" "+")
triple16
Gary is white.
True
2
proof
[(((triple14) -> rule4))]
("Gary" "is" "white" "+")
((triple14) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple14) -> rule4))]
("Gary" "is" "white" "-")
((triple14) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is nice.
True
4
proof
[(((triple4 ((triple3) -> rule4)) -> rule3) OR ((triple4 ((triple4) -> rule5)) -> rule3))]
("Dave" "is" "nice" "+")
((triple4 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((triple4 ((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not nice.
False
4
inv-proof
[(((triple4 ((triple3) -> rule4)) -> rule3) OR ((triple4 ((triple4) -> rule5)) -> rule3))]
("Dave" "is" "nice" "-")
((triple4 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((triple4 ((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "furry" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Dave is cold.[(triple1)] Dave is green.[(triple3)] Dave is not furry.[(triple2)] Dave is rough.[(triple4)] Erin is big.[(triple5)] Erin is furry.[(triple7)] Erin is green.[(triple8)] Erin is not cold.[(triple6)] Erin is not nice.[(triple9)] Erin is not rough.[(triple10)] Erin is white.[(triple11 OR ((triple8) -> rule4))] Gary is big.[(triple12)] Gary is green.[(triple14)] Gary is nice.[(triple15)] Gary is not cold.[(triple13)] Gary is not rough.[(triple16)] @1: Dave is white.[(((triple3) -> rule4) OR ((triple4) -> rule5))] Gary is white.[(((triple14) -> rule4))] @2: Dave is nice.[(((triple4 ((triple3) -> rule4)) -> rule3) OR ((triple4 ((triple4) -> rule5)) -> rule3))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is not furry.
("Dave" "is" "furry" "-")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is furry.
("Erin" "is" "furry" "+")
triple7
Erin is green.
("Erin" "is" "green" "+")
triple8
Erin is not cold.
("Erin" "is" "cold" "-")
triple6
Erin is not nice.
("Erin" "is" "nice" "-")
triple9
Erin is not rough.
("Erin" "is" "rough" "-")
triple10
Erin is white.
("Erin" "is" "white" "+")
triple11
((triple8) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple12
Gary is green.
("Gary" "is" "green" "+")
triple14
Gary is nice.
("Gary" "is" "nice" "+")
triple15
Gary is not cold.
("Gary" "is" "cold" "-")
triple13
Gary is not rough.
("Gary" "is" "rough" "-")
triple16
Dave is white.
("Dave" "is" "white" "+")
((triple3) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple4) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple14) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple4 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((triple4 ((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2