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