Erin is big. Erin is blue. Erin is nice. Erin is not white. Gary is big. Gary is not blue. Gary is cold. Gary is nice. Gary is rough. Harry is not blue. If Harry is not white then Harry is not blue. If Erin is cold then Erin is furry. White things are not nice. All cold, white things are big. If something is blue then it is big. If Erin is nice then Erin is cold. If something is rough and not big then it is furry. If something is furry then it is not rough.
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is not white.
("Erin" "is" "white" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
If Harry is not white then Harry is not blue.
((("Harry" "is" "white" "~")) -> ("Harry" "is" "blue" "-"))
If Erin is cold then Erin is furry.
((("Erin" "is" "cold" "+")) -> ("Erin" "is" "furry" "+"))
White things are not nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "-"))
All cold, white things are big.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If something is blue then it is big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If Erin is nice then Erin is cold.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "cold" "+"))
If something is rough and not big then it is furry.
((("something" "is" "rough" "+") ("something" "is" "big" "~")) -> ("something" "is" "furry" "+"))
If something is furry then it is not rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "-"))
Gary is big.
True
1
proof
[(triple5)]
("Gary" "is" "big" "+")
triple5
Gary is not rough.
False
1
inv-proof
[(triple9)]
("Gary" "is" "rough" "-")
triple9
Erin is cold.
True
2
proof
[(((triple3) -> rule6))]
("Erin" "is" "cold" "+")
((triple3) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not cold.
False
2
inv-proof
[(((triple3) -> rule6))]
("Erin" "is" "cold" "-")
((triple3) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
True
3
proof
[(((((triple3) -> rule6)) -> rule2))]
("Erin" "is" "furry" "+")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not furry.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule2))]
("Erin" "is" "furry" "-")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not rough.
True
4
proof
[(((((((triple3) -> rule6)) -> rule2)) -> rule8))]
("Erin" "is" "rough" "-")
((((((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is rough.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule2)) -> rule8))]
("Erin" "is" "rough" "+")
((((((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Harry is not furry.
Unknown
inv-rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "furry" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "big" "+")
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "furry" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Erin is big.[(triple1 OR ((triple2) -> rule5))] Erin is blue.[(triple2)] Erin is nice.[(triple3)] Erin is not white.[(triple4)] Gary is big.[(triple5)] Gary is cold.[(triple7)] Gary is nice.[(triple8)] Gary is not blue.[(triple6)] Gary is rough.[(triple9)] Harry is not blue.[(triple10)] @1: Erin is cold.[(((triple3) -> rule6))] @2: Erin is furry.[(((((triple3) -> rule6)) -> rule2))] @3: Erin is not rough.[(((((((triple3) -> rule6)) -> rule2)) -> rule8))]
Erin is big.
("Erin" "is" "big" "+")
triple1
((triple2) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Erin is not white.
("Erin" "is" "white" "-")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
Gary is cold.
("Gary" "is" "cold" "+")
triple7
Gary is nice.
("Gary" "is" "nice" "+")
triple8
Gary is not blue.
("Gary" "is" "blue" "-")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple9
Harry is not blue.
("Harry" "is" "blue" "-")
triple10
Erin is cold.
("Erin" "is" "cold" "+")
((triple3) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not rough.
("Erin" "is" "rough" "-")
((((((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3