Anne is red. Anne is rough. Dave is young. Erin is nice. Erin is young. Gary is nice. Gary is young. All cold, nice things are rough. If something is smart then it is cold. If something is furry and smart then it is cold. If Gary is furry and Gary is rough then Gary is red. If something is nice and not young then it is red. If something is nice and cold then it is red. Furry things are nice. If something is young then it is smart.
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is young.
("Gary" "is" "young" "+")
All cold, nice things are rough.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If something is smart then it is cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
If something is furry and smart then it is cold.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
If Gary is furry and Gary is rough then Gary is red.
((("Gary" "is" "furry" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "red" "+"))
If something is nice and not young then it is red.
((("something" "is" "nice" "+") ("something" "is" "young" "~")) -> ("something" "is" "red" "+"))
If something is nice and cold then it is red.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Furry things are nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If something is young then it is smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
Gary is nice.
True
1
proof
[(triple6)]
("Gary" "is" "nice" "+")
triple6
Gary is not nice.
False
1
inv-proof
[(triple6)]
("Gary" "is" "nice" "-")
triple6
Dave is smart.
True
2
proof
[(((triple3) -> rule8))]
("Dave" "is" "smart" "+")
((triple3) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple5) -> rule8))]
("Erin" "is" "smart" "-")
((triple5) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Dave is cold.
True
3
proof
[(((((triple3) -> rule8)) -> rule2))]
("Dave" "is" "cold" "+")
((((triple3) -> (rule8 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Gary is not cold.
False
3
inv-proof
[(((((triple7) -> rule8)) -> rule2))]
("Gary" "is" "cold" "-")
((((triple7) -> (rule8 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
True
5
proof
[(((((((triple7) -> rule8)) -> rule2) triple6) -> rule1))]
("Gary" "is" "rough" "+")
((((((triple7) -> (rule8 % int3))) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not red.
False
5
inv-proof
[(((triple6 ((((triple7) -> rule8)) -> rule2)) -> rule6))]
("Gary" "is" "red" "-")
((triple6 ((((triple7) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "nice" "-")
Anne is smart.
Unknown
rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "smart" "+")
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "nice" "-")
Dave is red.
Unknown
rconc
[@2: Dave is red.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Dave" "is" "red" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is red.[(triple1)] Anne is rough.[(triple2)] Dave is young.[(triple3)] Erin is nice.[(triple4)] Erin is young.[(triple5)] Gary is nice.[(triple6)] Gary is young.[(triple7)] @1: Dave is smart.[(((triple3) -> rule8))] Erin is smart.[(((triple5) -> rule8))] Gary is smart.[(((triple7) -> rule8))] @2: Dave is cold.[(((((triple3) -> rule8)) -> rule2))] Erin is cold.[(((((triple5) -> rule8)) -> rule2))] Gary is cold.[(((((triple7) -> rule8)) -> rule2))] @3: Erin is red.[(((triple4 ((((triple5) -> rule8)) -> rule2)) -> rule6))] Erin is rough.[(((((((triple5) -> rule8)) -> rule2) triple4) -> rule1))] Gary is red.[(((triple6 ((((triple7) -> rule8)) -> rule2)) -> rule6))] Gary is rough.[(((((((triple7) -> rule8)) -> rule2) triple6) -> rule1))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Dave is smart.
("Dave" "is" "smart" "+")
((triple3) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple5) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple7) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple3) -> (rule8 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((triple5) -> (rule8 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((triple7) -> (rule8 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((triple4 ((((triple5) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
((((((triple5) -> (rule8 % int3))) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((triple6 ((((triple7) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
((((((triple7) -> (rule8 % int3))) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3