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