Anne is rough. Anne is young. Bob is not rough. Erin is furry. Erin is red. Gary is big. Gary is not rough. If Gary is young then Gary is red. If something is big then it is young. If Bob is blue then Bob is red. Nice things are blue. Red things are not nice. If something is young and nice then it is not red. If something is furry and not red then it is rough. If something is red and not blue then it is rough.
Anne is rough.
("Anne" "is" "rough" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is red.
("Erin" "is" "red" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
If Gary is young then Gary is red.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "red" "+"))
If something is big then it is young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If Bob is blue then Bob is red.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "red" "+"))
Nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Red things are not nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "-"))
If something is young and nice then it is not red.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "-"))
If something is furry and not red then it is rough.
((("something" "is" "furry" "+") ("something" "is" "red" "~")) -> ("something" "is" "rough" "+"))
If something is red and not blue then it is rough.
((("something" "is" "red" "+") ("something" "is" "blue" "~")) -> ("something" "is" "rough" "+"))
Erin is furry.
True
1
proof
[(triple4)]
("Erin" "is" "furry" "+")
triple4
Gary is not big.
False
1
inv-proof
[(triple6)]
("Gary" "is" "big" "-")
triple6
Erin is not nice.
True
2
proof
[(((triple5) -> rule5))]
("Erin" "is" "nice" "-")
((triple5) -> (rule5 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Gary is not young.
False
2
inv-proof
[(((triple6) -> rule2))]
("Gary" "is" "young" "-")
((triple6) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
True
3
proof
[(((((triple6) -> rule2)) -> rule1))]
("Gary" "is" "red" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not red.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule1))]
("Gary" "is" "red" "-")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not nice.
True
4
proof
[(((((((triple6) -> rule2)) -> rule1)) -> rule5))]
("Gary" "is" "nice" "-")
((((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is nice.
False
4
inv-proof
[(((((((triple6) -> rule2)) -> rule1)) -> rule5))]
("Gary" "is" "nice" "+")
((((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "blue" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "rough" "+")
Bob is not red.
Unknown
inv-rconc
[@2: Bob is red.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Bob" "is" "red" "-")
Bob is blue.
Unknown
rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "blue" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Anne is rough.[(triple1)] Anne is young.[(triple2)] Bob is not rough.[(triple3)] Erin is furry.[(triple4)] Erin is red.[(triple5)] Gary is big.[(triple6)] Gary is not rough.[(triple7)] @1: Erin is not nice.[(((triple5) -> rule5))] Gary is young.[(((triple6) -> rule2))] @2: Gary is red.[(((((triple6) -> rule2)) -> rule1))] @3: Gary is not nice.[(((((((triple6) -> rule2)) -> rule1)) -> rule5))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Bob is not rough.
("Bob" "is" "rough" "-")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is not rough.
("Gary" "is" "rough" "-")
triple7
Erin is not nice.
("Erin" "is" "nice" "-")
((triple5) -> (rule5 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple6) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not nice.
("Gary" "is" "nice" "-")
((((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3