Anne is nice. Anne is red. Dave is furry. Dave is kind. Dave is white. Erin is furry. Erin is white. Harry is kind. Harry is red. Harry is white. All young people are green. Nice, young people are furry. If someone is kind then they are white. If Dave is furry then Dave is green. All furry people are kind. If someone is green then they are young. Young people are green. Kind, red people are white. Nice people are green.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
All young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Nice, young people are furry.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
If someone is kind then they are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
If Dave is furry then Dave is green.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "green" "+"))
All furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If someone is green then they are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
Young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Kind, red people are white.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Erin is white.
True
1
proof
[(triple7 OR ((((triple6) -> rule5)) -> rule3))]
("Erin" "is" "white" "+")
triple7
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Harry is not kind.
False
1
inv-proof
[(triple8)]
("Harry" "is" "kind" "-")
triple8
Erin is kind.
True
2
proof
[(((triple6) -> rule5))]
("Erin" "is" "kind" "+")
((triple6) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple3) -> rule4))]
("Dave" "is" "green" "-")
((triple3) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Anne is young.
True
3
proof
[(((((triple1) -> rule9)) -> rule6))]
("Anne" "is" "young" "+")
((((triple1) -> (rule9 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not young.
False
3
inv-proof
[(((((triple1) -> rule9)) -> rule6))]
("Anne" "is" "young" "-")
((((triple1) -> (rule9 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is furry.
True
5
proof
[(((triple1 ((((triple1) -> rule9)) -> rule6)) -> rule2))]
("Anne" "is" "furry" "+")
((triple1 ((((triple1) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not furry.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule9)) -> rule6)) -> rule2))]
("Anne" "is" "furry" "-")
((triple1 ((((triple1) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is kind.
True
6
proof
[(((((triple1 ((((triple1) -> rule9)) -> rule6)) -> rule2)) -> rule5))]
("Anne" "is" "kind" "+")
((((triple1 ((((triple1) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is not kind.
False
6
inv-proof
[(((((triple1 ((((triple1) -> rule9)) -> rule6)) -> rule2)) -> rule5))]
("Anne" "is" "kind" "-")
((((triple1 ((((triple1) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is white.
True
7
proof
[(((((((triple1 ((((triple1) -> rule9)) -> rule6)) -> rule2)) -> rule5)) -> rule3) OR ((((((triple1 ((((triple1) -> rule9)) -> rule6)) -> rule2)) -> rule5) triple2) -> rule8))]
("Anne" "is" "white" "+")
((((((triple1 ((((triple1) -> (rule9 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
((((((triple1 ((((triple1) -> (rule9 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) triple2) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
Anne is not white.
False
7
inv-proof
[(((((((triple1 ((((triple1) -> rule9)) -> rule6)) -> rule2)) -> rule5)) -> rule3) OR ((((((triple1 ((((triple1) -> rule9)) -> rule6)) -> rule2)) -> rule5) triple2) -> rule8))]
("Anne" "is" "white" "-")
((((((triple1 ((((triple1) -> (rule9 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
((((((triple1 ((((triple1) -> (rule9 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) triple2) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
Harry is not green.
Unknown
inv-rconc
[@3: Harry is green.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule7 <- FAIL)]]
("Harry" "is" "green" "-")
Erin is young.
Unknown
rconc
[@2: Erin is young.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Erin" "is" "young" "+")
Harry is not young.
Unknown
inv-rconc
[@2: Harry is young.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Harry" "is" "young" "-")
Erin is green.
Unknown
rconc
[@3: Erin is green.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule7 <- FAIL)]]
("Erin" "is" "green" "+")
Harry is not furry.
Unknown
inv-rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "furry" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Anne is nice.[(triple1)] Anne is red.[(triple2)] Dave is furry.[(triple3)] Dave is kind.[(triple4 OR ((triple3) -> rule5))] Dave is white.[(triple5 OR ((triple4) -> rule3) OR ((((triple3) -> rule5)) -> rule3))] Erin is furry.[(triple6)] Erin is white.[(triple7 OR ((((triple6) -> rule5)) -> rule3))] Harry is kind.[(triple8)] Harry is red.[(triple9)] Harry is white.[(triple10 OR ((triple8) -> rule3) OR ((triple8 triple9) -> rule8))] @1: Anne is green.[(((triple1) -> rule9))] Dave is green.[(((triple3) -> rule4))] Erin is kind.[(((triple6) -> rule5))] @2: Anne is young.[(((((triple1) -> rule9)) -> rule6))] Dave is young.[(((((triple3) -> rule4)) -> rule6))] @3: Anne is furry.[(((triple1 ((((triple1) -> rule9)) -> rule6)) -> rule2))] @4: Anne is kind.[(((((triple1 ((((triple1) -> rule9)) -> rule6)) -> rule2)) -> rule5))] @5: Anne is white.[(((((((triple1 ((((triple1) -> rule9)) -> rule6)) -> rule2)) -> rule5)) -> rule3) OR ((((((triple1 ((((triple1) -> rule9)) -> rule6)) -> rule2)) -> rule5) triple2) -> rule8))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
((triple3) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple5
((triple4) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple8
Harry is red.
("Harry" "is" "red" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
((triple8) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple8 triple9) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule9 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple3) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple6) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule9 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((triple1 ((((triple1) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1 ((((triple1) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
((((((triple1 ((((triple1) -> (rule9 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
((((((triple1 ((((triple1) -> (rule9 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) triple2) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5