Erin is furry. Erin is rough. Erin is not white. Erin is young. Gary is blue. Gary is cold. Gary is furry. Gary is not green. Gary is rough. Gary is white. Gary is young. Harry is blue. Harry is cold. Harry is green. Harry is rough. Harry is young. Green people are rough. If Erin is not furry then Erin is white. If Erin is cold and Erin is not green then Erin is not rough. If someone is white and blue then they are cold. If someone is furry and not white then they are cold. If someone is furry and not white then they are blue.
Erin is furry.
("Erin" "is" "furry" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is not white.
("Erin" "is" "white" "-")
Erin is young.
("Erin" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is not green.
("Gary" "is" "green" "-")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is young.
("Harry" "is" "young" "+")
Green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If Erin is not furry then Erin is white.
((("Erin" "is" "furry" "~")) -> ("Erin" "is" "white" "+"))
If Erin is cold and Erin is not green then Erin is not rough.
((("Erin" "is" "cold" "+") ("Erin" "is" "green" "~")) -> ("Erin" "is" "rough" "-"))
If someone is white and blue then they are cold.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If someone is furry and not white then they are cold.
((("someone" "is" "furry" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "cold" "+"))
If someone is furry and not white then they are blue.
((("someone" "is" "furry" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "blue" "+"))
Erin is furry.
True
1
proof
[(triple1)]
("Erin" "is" "furry" "+")
triple1
Gary is green.
False
1
inv-proof
[(triple8)]
("Gary" "is" "green" "+")
triple8
Erin is cold.
True
3
proof
[(((triple1 triple3) -> rule5))]
("Erin" "is" "cold" "+")
((triple1 triple3) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not cold.
False
3
inv-proof
[(((triple1 triple3) -> rule5))]
("Erin" "is" "cold" "-")
((triple1 triple3) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Erin is furry.[(triple1)] Erin is not white.[(triple3)] Erin is rough.[(triple2)] Erin is young.[(triple4)] Gary is blue.[(triple5)] Gary is cold.[(triple6 OR ((triple10 triple5) -> rule4))] Gary is furry.[(triple7)] Gary is not green.[(triple8)] Gary is rough.[(triple9)] Gary is white.[(triple10)] Gary is young.[(triple11)] Harry is blue.[(triple12)] Harry is cold.[(triple13)] Harry is green.[(triple14)] Harry is rough.[(triple15 OR ((triple14) -> rule1))] Harry is young.[(triple16)] @1: Erin is blue.[(((triple1 triple3) -> rule6))] Erin is cold.[(((triple1 triple3) -> rule5))]
Erin is furry.
("Erin" "is" "furry" "+")
triple1
Erin is not white.
("Erin" "is" "white" "-")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
Gary is cold.
("Gary" "is" "cold" "+")
triple6
((triple10 triple5) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple7
Gary is not green.
("Gary" "is" "green" "-")
triple8
Gary is rough.
("Gary" "is" "rough" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Gary is young.
("Gary" "is" "young" "+")
triple11
Harry is blue.
("Harry" "is" "blue" "+")
triple12
Harry is cold.
("Harry" "is" "cold" "+")
triple13
Harry is green.
("Harry" "is" "green" "+")
triple14
Harry is rough.
("Harry" "is" "rough" "+")
triple15
((triple14) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple16
Erin is blue.
("Erin" "is" "blue" "+")
((triple1 triple3) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple1 triple3) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1