Anne is kind. Dave is green. Dave is quiet. Dave is red. Dave is round. Dave is young. Fiona is green. Fiona is red. Harry is green. Harry is not quiet. If something is green then it is big. Round, quiet things are big. Red things are quiet. If Fiona is big then Fiona is round. All kind things are round. If something is red and green then it is round. If something is big and not kind then it is young. If something is big then it is young. If something is round then it is red.
Anne is kind.
("Anne" "is" "kind" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
If something is green then it is big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
Round, quiet things are big.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
Red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If Fiona is big then Fiona is round.
((("Fiona" "is" "big" "+")) -> ("Fiona" "is" "round" "+"))
All kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If something is red and green then it is round.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If something is big and not kind then it is young.
((("something" "is" "big" "+") ("something" "is" "kind" "~")) -> ("something" "is" "young" "+"))
If something is big then it is young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is round then it is red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Dave is green.
True
1
proof
[(triple2)]
("Dave" "is" "green" "+")
triple2
Dave is not green.
False
1
inv-proof
[(triple2)]
("Dave" "is" "green" "-")
triple2
Anne is round.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "round" "+")
((triple1) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple9) -> rule1))]
("Harry" "is" "big" "-")
((triple9) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Fiona is young.
True
3
proof
[(((((triple7) -> rule1)) -> rule8) OR ((((((triple8 triple7) -> rule6) ((triple8) -> rule3)) -> rule2)) -> rule8))]
("Fiona" "is" "young" "+")
((((triple7) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((((triple8 triple7) -> (rule6 % int4)) ((triple8) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Anne is not red.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule9))]
("Anne" "is" "red" "-")
((((triple1) -> (rule5 % int2))) -> (rule9 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is quiet.
True
4
proof
[(((((((triple1) -> rule5)) -> rule9)) -> rule3))]
("Anne" "is" "quiet" "+")
((((((triple1) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not quiet.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule9)) -> rule3))]
("Anne" "is" "quiet" "-")
((((((triple1) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is big.
True
7
proof
[(((((triple1) -> rule5) ((((((triple1) -> rule5)) -> rule9)) -> rule3)) -> rule2))]
("Anne" "is" "big" "+")
((((triple1) -> (rule5 % int4)) ((((((triple1) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is not big.
False
7
inv-proof
[(((((triple1) -> rule5) ((((((triple1) -> rule5)) -> rule9)) -> rule3)) -> rule2))]
("Anne" "is" "big" "-")
((((triple1) -> (rule5 % int4)) ((((((triple1) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is young.
True
8
proof
[(((((((triple1) -> rule5) ((((((triple1) -> rule5)) -> rule9)) -> rule3)) -> rule2)) -> rule8))]
("Anne" "is" "young" "+")
((((((triple1) -> (rule5 % int5)) ((((((triple1) -> (rule5 % int5))) -> (rule9 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
Anne is not young.
False
8
inv-proof
[(((((((triple1) -> rule5) ((((((triple1) -> rule5)) -> rule9)) -> rule3)) -> rule2)) -> rule8))]
("Anne" "is" "young" "-")
((((((triple1) -> (rule5 % int5)) ((((((triple1) -> (rule5 % int5))) -> (rule9 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
Harry is not round.
Unknown
inv-rconc
[@3: Harry is round.[CWA. Example of deepest failure = (rule6 <- rule9 <- rule5 <- FAIL)]]
("Harry" "is" "round" "-")
Harry is red.
Unknown
rconc
[@2: Harry is red.[CWA. Example of deepest failure = (rule9 <- rule5 <- FAIL)]]
("Harry" "is" "red" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Anne is kind.[(triple1)] Dave is green.[(triple2)] Dave is quiet.[(triple3 OR ((triple4) -> rule3) OR ((((triple5) -> rule9)) -> rule3))] Dave is red.[(triple4 OR ((triple5) -> rule9))] Dave is round.[(triple5 OR ((triple4 triple2) -> rule6))] Dave is young.[(triple6 OR ((((triple2) -> rule1)) -> rule8) OR ((((triple5 triple3) -> rule2)) -> rule8) OR ((((triple5 ((triple4) -> rule3)) -> rule2)) -> rule8) OR ((((((triple4 triple2) -> rule6) triple3) -> rule2)) -> rule8) OR ((((((triple4 triple2) -> rule6) ((triple4) -> rule3)) -> rule2)) -> rule8) OR ((((triple5 ((((triple5) -> rule9)) -> rule3)) -> rule2)) -> rule8) OR ((((((triple4 triple2) -> rule6) ((((triple5) -> rule9)) -> rule3)) -> rule2)) -> rule8))] Fiona is green.[(triple7)] Fiona is red.[(triple8 OR ((((((triple7) -> rule1)) -> rule4)) -> rule9))] Harry is green.[(triple9)] Harry is not quiet.[(triple10)] @1: Anne is round.[(((triple1) -> rule5))] Dave is big.[(((triple2) -> rule1) OR ((triple5 triple3) -> rule2) OR ((triple5 ((triple4) -> rule3)) -> rule2) OR ((((triple4 triple2) -> rule6) triple3) -> rule2) OR ((((triple4 triple2) -> rule6) ((triple4) -> rule3)) -> rule2) OR ((triple5 ((((triple5) -> rule9)) -> rule3)) -> rule2) OR ((((triple4 triple2) -> rule6) ((((triple5) -> rule9)) -> rule3)) -> rule2))] Fiona is big.[(((triple7) -> rule1) OR ((((triple8 triple7) -> rule6) ((triple8) -> rule3)) -> rule2))] Fiona is quiet.[(((triple8) -> rule3) OR ((((((((triple7) -> rule1)) -> rule4)) -> rule9)) -> rule3))] Fiona is round.[(((triple8 triple7) -> rule6) OR ((((triple7) -> rule1)) -> rule4))] Harry is big.[(((triple9) -> rule1))] @2: Anne is red.[(((((triple1) -> rule5)) -> rule9))] Fiona is young.[(((((triple7) -> rule1)) -> rule8) OR ((((((triple8 triple7) -> rule6) ((triple8) -> rule3)) -> rule2)) -> rule8))] Harry is young.[(((((triple9) -> rule1)) -> rule8))] @3: Anne is quiet.[(((((((triple1) -> rule5)) -> rule9)) -> rule3))] @4: Anne is big.[(((((triple1) -> rule5) ((((((triple1) -> rule5)) -> rule9)) -> rule3)) -> rule2))] @5: Anne is young.[(((((((triple1) -> rule5) ((((((triple1) -> rule5)) -> rule9)) -> rule3)) -> rule2)) -> rule8))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
((triple4) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple5) -> (rule9 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple4
((triple5) -> (rule9 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple5
((triple4 triple2) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple6
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple5 triple3) -> (rule2 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple5 ((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((((triple4 triple2) -> (rule6 % int3)) triple3) -> (rule2 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((((triple4 triple2) -> (rule6 % int4)) ((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((triple5 ((((triple5) -> (rule9 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
((((((triple4 triple2) -> (rule6 % int5)) ((((triple5) -> (rule9 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
int5
Fiona is green.
("Fiona" "is" "green" "+")
triple7
Fiona is red.
("Fiona" "is" "red" "+")
triple8
((((((triple7) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple10
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple2) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple5 triple3) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple5 ((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple4 triple2) -> (rule6 % int2)) triple3) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple4 triple2) -> (rule6 % int3)) ((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((triple5 ((((triple5) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((triple4 triple2) -> (rule6 % int4)) ((((triple5) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
((triple7) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((triple8 triple7) -> (rule6 % int3)) ((triple8) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple8) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((((((triple7) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Fiona is round.
("Fiona" "is" "round" "+")
((triple8 triple7) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((triple9) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule5 % int2))) -> (rule9 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((triple7) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((((triple8 triple7) -> (rule6 % int4)) ((triple8) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Harry is young.
("Harry" "is" "young" "+")
((((triple9) -> (rule1 % int2))) -> (rule8 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((((triple1) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule5 % int4)) ((((((triple1) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
((((((triple1) -> (rule5 % int5)) ((((((triple1) -> (rule5 % int5))) -> (rule9 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5