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