Anne is not green. Anne is round. Dave is nice. Dave is young. Erin is not green. Erin is not kind. Erin is not nice. Erin is not smart. Erin is young. Gary is green. Gary is nice. Gary is young. Green people are not round. If someone is nice then they are green. If Anne is big then Anne is not kind. If someone is young and not round then they are smart. If someone is smart then they are big. Big people are not kind.
Anne is not green.
("Anne" "is" "green" "-")
Anne is round.
("Anne" "is" "round" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is not green.
("Erin" "is" "green" "-")
Erin is not kind.
("Erin" "is" "kind" "-")
Erin is not nice.
("Erin" "is" "nice" "-")
Erin is not smart.
("Erin" "is" "smart" "-")
Erin is young.
("Erin" "is" "young" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is young.
("Gary" "is" "young" "+")
Green people are not round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "-"))
If someone is nice then they are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If Anne is big then Anne is not kind.
((("Anne" "is" "big" "+")) -> ("Anne" "is" "kind" "-"))
If someone is young and not round then they are smart.
((("someone" "is" "young" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "smart" "+"))
If someone is smart then they are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Big people are not kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "-"))
Erin is not green.
True
1
proof
[(triple5)]
("Erin" "is" "green" "-")
triple5
Erin is not young.
False
1
inv-proof
[(triple9)]
("Erin" "is" "young" "-")
triple9
Dave is green.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "green" "+")
((triple3) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "green" "-")
((triple3) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not round.
True
3
proof
[(((((triple3) -> rule2)) -> rule1))]
("Dave" "is" "round" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is round.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("Dave" "is" "round" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is smart.
True
5
proof
[(((triple4 ((((triple3) -> rule2)) -> rule1)) -> rule4))]
("Dave" "is" "smart" "+")
((triple4 ((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not round.
("Dave" "is" "round" "-")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is not smart.
False
5
inv-proof
[(((triple4 ((((triple3) -> rule2)) -> rule1)) -> rule4))]
("Dave" "is" "smart" "-")
((triple4 ((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not round.
("Dave" "is" "round" "-")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is big.
True
6
proof
[(((((triple4 ((((triple3) -> rule2)) -> rule1)) -> rule4)) -> rule5))]
("Dave" "is" "big" "+")
((((triple4 ((((triple3) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not round.
("Dave" "is" "round" "-")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is not big.
False
6
inv-proof
[(((((triple4 ((((triple3) -> rule2)) -> rule1)) -> rule4)) -> rule5))]
("Dave" "is" "big" "-")
((((triple4 ((((triple3) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not round.
("Dave" "is" "round" "-")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is not kind.
True
7
proof
[(((((((triple4 ((((triple3) -> rule2)) -> rule1)) -> rule4)) -> rule5)) -> rule6))]
("Dave" "is" "kind" "-")
((((((triple4 ((((triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is not round.
("Dave" "is" "round" "-")
int4
Dave is green.
("Dave" "is" "green" "+")
int5
Dave is kind.
False
7
inv-proof
[(((((((triple4 ((((triple3) -> rule2)) -> rule1)) -> rule4)) -> rule5)) -> rule6))]
("Dave" "is" "kind" "+")
((((((triple4 ((((triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is not round.
("Dave" "is" "round" "-")
int4
Dave is green.
("Dave" "is" "green" "+")
int5
Anne is not big.
Unknown
inv-rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Anne" "is" "big" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "big" "+")
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "smart" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Anne is not green.[(triple1)] Anne is round.[(triple2)] Dave is nice.[(triple3)] Dave is young.[(triple4)] Erin is not green.[(triple5)] Erin is not kind.[(triple6)] Erin is not nice.[(triple7)] Erin is not smart.[(triple8)] Erin is young.[(triple9)] Gary is green.[(triple10 OR ((triple11) -> rule2))] Gary is nice.[(triple11)] Gary is young.[(triple12)] @1: Dave is green.[(((triple3) -> rule2))] Gary is not round.[(((triple10) -> rule1) OR ((((triple11) -> rule2)) -> rule1))] @2: Dave is not round.[(((((triple3) -> rule2)) -> rule1))] Gary is smart.[(((triple12 ((triple10) -> rule1)) -> rule4) OR ((triple12 ((((triple11) -> rule2)) -> rule1)) -> rule4))] @3: Dave is smart.[(((triple4 ((((triple3) -> rule2)) -> rule1)) -> rule4))] Gary is big.[(((((triple12 ((triple10) -> rule1)) -> rule4)) -> rule5) OR ((((triple12 ((((triple11) -> rule2)) -> rule1)) -> rule4)) -> rule5))] @4: Dave is big.[(((((triple4 ((((triple3) -> rule2)) -> rule1)) -> rule4)) -> rule5))] Gary is not kind.[(((((((triple12 ((triple10) -> rule1)) -> rule4)) -> rule5)) -> rule6) OR ((((((triple12 ((((triple11) -> rule2)) -> rule1)) -> rule4)) -> rule5)) -> rule6))] @5: Dave is not kind.[(((((((triple4 ((((triple3) -> rule2)) -> rule1)) -> rule4)) -> rule5)) -> rule6))]
Anne is not green.
("Anne" "is" "green" "-")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Erin is not green.
("Erin" "is" "green" "-")
triple5
Erin is not kind.
("Erin" "is" "kind" "-")
triple6
Erin is not nice.
("Erin" "is" "nice" "-")
triple7
Erin is not smart.
("Erin" "is" "smart" "-")
triple8
Erin is young.
("Erin" "is" "young" "+")
triple9
Gary is green.
("Gary" "is" "green" "+")
triple10
((triple11) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
Dave is green.
("Dave" "is" "green" "+")
((triple3) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Gary is not round.
("Gary" "is" "round" "-")
((triple10) -> (rule1 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
((((triple11) -> (rule2 % int2))) -> (rule1 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Dave is not round.
("Dave" "is" "round" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((triple12 ((triple10) -> (rule1 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not round.
("Gary" "is" "round" "-")
int2
((triple12 ((((triple11) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not round.
("Gary" "is" "round" "-")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((triple4 ((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not round.
("Dave" "is" "round" "-")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
((((triple12 ((triple10) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not round.
("Gary" "is" "round" "-")
int3
((((triple12 ((((triple11) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not round.
("Gary" "is" "round" "-")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Dave is big.
("Dave" "is" "big" "+")
((((triple4 ((((triple3) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not round.
("Dave" "is" "round" "-")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Gary is not kind.
("Gary" "is" "kind" "-")
((((((triple12 ((triple10) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not round.
("Gary" "is" "round" "-")
int4
((((((triple12 ((((triple11) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not round.
("Gary" "is" "round" "-")
int4
Gary is green.
("Gary" "is" "green" "+")
int5
Dave is not kind.
("Dave" "is" "kind" "-")
((((((triple4 ((((triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is not round.
("Dave" "is" "round" "-")
int4
Dave is green.
("Dave" "is" "green" "+")
int5