Anne is furry. Anne is green. Anne is rough. Bob is nice. Dave is smart. Erin is big. Erin is green. Furry things are green. Nice things are rough. All furry, nice things are green. Nice things are big. All rough things are nice. All smart, green things are big. If something is kind and smart then it is rough. If Erin is rough and Erin is furry then Erin is green.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
Furry things are green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
Nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
All furry, nice things are green.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All smart, green things are big.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is kind and smart then it is rough.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If Erin is rough and Erin is furry then Erin is green.
((("Erin" "is" "rough" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "green" "+"))
Erin is big.
True
1
proof
[(triple6)]
("Erin" "is" "big" "+")
triple6
Bob is not nice.
False
1
inv-proof
[(triple4)]
("Bob" "is" "nice" "-")
triple4
Bob is rough.
True
2
proof
[(((triple4) -> rule2))]
("Bob" "is" "rough" "+")
((triple4) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple3) -> rule5))]
("Anne" "is" "nice" "-")
((triple3) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
True
3
proof
[(((((triple3) -> rule5)) -> rule4))]
("Anne" "is" "big" "+")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not big.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule4))]
("Anne" "is" "big" "-")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Dave is not nice.
Unknown
inv-rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Dave" "is" "nice" "-")
Erin is nice.
Unknown
rconc
[@2: Erin is nice.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Erin" "is" "nice" "+")
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "green" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is furry.[(triple1)] Anne is green.[(triple2 OR ((triple1) -> rule1) OR ((triple1 ((triple3) -> rule5)) -> rule3))] Anne is rough.[(triple3)] Bob is nice.[(triple4)] Dave is smart.[(triple5)] Erin is big.[(triple6)] Erin is green.[(triple7)] @1: Anne is nice.[(((triple3) -> rule5))] Bob is big.[(((triple4) -> rule4))] Bob is rough.[(((triple4) -> rule2))] @2: Anne is big.[(((((triple3) -> rule5)) -> rule4))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple1 ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Erin is big.
("Erin" "is" "big" "+")
triple6
Erin is green.
("Erin" "is" "green" "+")
triple7
Anne is nice.
("Anne" "is" "nice" "+")
((triple3) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((triple4) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple4) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2