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