Anne is quiet. Bob is blue. Bob is kind. Bob is young. Charlie is quiet. Charlie is young. Erin is quiet. If someone is quiet and kind then they are young. Blue people are young. All quiet, white people are furry. All young, kind people are blue. All furry people are kind. All quiet people are white.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
If someone is quiet and kind then they are young.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
Blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
All quiet, white people are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
All young, kind people are blue.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
All furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
All quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Erin is quiet.
True
1
proof
[(triple7)]
("Erin" "is" "quiet" "+")
triple7
Bob is not young.
False
1
inv-proof
[(triple4 OR ((triple2) -> rule2))]
("Bob" "is" "young" "-")
triple4
((triple2) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Erin is white.
True
2
proof
[(((triple7) -> rule6))]
("Erin" "is" "white" "+")
((triple7) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is not white.
False
2
inv-proof
[(((triple7) -> rule6))]
("Erin" "is" "white" "-")
((triple7) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Charlie is furry.
True
4
proof
[(((triple5 ((triple5) -> rule6)) -> rule3))]
("Charlie" "is" "furry" "+")
((triple5 ((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Erin is not furry.
False
4
inv-proof
[(((triple7 ((triple7) -> rule6)) -> rule3))]
("Erin" "is" "furry" "-")
((triple7 ((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Anne is kind.
True
5
proof
[(((((triple1 ((triple1) -> rule6)) -> rule3)) -> rule5))]
("Anne" "is" "kind" "+")
((((triple1 ((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Erin is not kind.
False
5
inv-proof
[(((((triple7 ((triple7) -> rule6)) -> rule3)) -> rule5))]
("Erin" "is" "kind" "-")
((((triple7 ((triple7) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Charlie is blue.
True
7
proof
[(((triple6 ((((triple5 ((triple5) -> rule6)) -> rule3)) -> rule5)) -> rule4) OR ((((triple5 ((((triple5 ((triple5) -> rule6)) -> rule3)) -> rule5)) -> rule1) ((((triple5 ((triple5) -> rule6)) -> rule3)) -> rule5)) -> rule4))]
("Charlie" "is" "blue" "+")
((triple6 ((((triple5 ((triple5) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
((((triple5 ((((triple5 ((triple5) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((((triple5 ((triple5) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
int5
Anne is not young.
False
7
inv-proof
[(((triple1 ((((triple1 ((triple1) -> rule6)) -> rule3)) -> rule5)) -> rule1))]
("Anne" "is" "young" "-")
((triple1 ((((triple1 ((triple1) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is blue.
True
13
proof
[(((((triple1 ((((triple1 ((triple1) -> rule6)) -> rule3)) -> rule5)) -> rule1) ((((triple1 ((triple1) -> rule6)) -> rule3)) -> rule5)) -> rule4))]
("Anne" "is" "blue" "+")
((((triple1 ((((triple1 ((triple1) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((((triple1 ((triple1) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
int5
Erin is not blue.
False
13
inv-proof
[(((((triple7 ((((triple7 ((triple7) -> rule6)) -> rule3)) -> rule5)) -> rule1) ((((triple7 ((triple7) -> rule6)) -> rule3)) -> rule5)) -> rule4))]
("Erin" "is" "blue" "-")
((((triple7 ((((triple7 ((triple7) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((((triple7 ((triple7) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "furry" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "white" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Anne is quiet.[(triple1)] Bob is blue.[(triple2 OR ((triple4 triple3) -> rule4))] Bob is kind.[(triple3)] Bob is young.[(triple4 OR ((triple2) -> rule2))] Charlie is quiet.[(triple5)] Charlie is young.[(triple6 OR ((triple5 ((((triple5 ((triple5) -> rule6)) -> rule3)) -> rule5)) -> rule1))] Erin is quiet.[(triple7)] @1: Anne is white.[(((triple1) -> rule6))] Charlie is white.[(((triple5) -> rule6))] Erin is white.[(((triple7) -> rule6))] @2: Anne is furry.[(((triple1 ((triple1) -> rule6)) -> rule3))] Charlie is furry.[(((triple5 ((triple5) -> rule6)) -> rule3))] Erin is furry.[(((triple7 ((triple7) -> rule6)) -> rule3))] @3: Anne is kind.[(((((triple1 ((triple1) -> rule6)) -> rule3)) -> rule5))] Charlie is kind.[(((((triple5 ((triple5) -> rule6)) -> rule3)) -> rule5))] Erin is kind.[(((((triple7 ((triple7) -> rule6)) -> rule3)) -> rule5))] @4: Anne is young.[(((triple1 ((((triple1 ((triple1) -> rule6)) -> rule3)) -> rule5)) -> rule1))] Charlie is blue.[(((triple6 ((((triple5 ((triple5) -> rule6)) -> rule3)) -> rule5)) -> rule4) OR ((((triple5 ((((triple5 ((triple5) -> rule6)) -> rule3)) -> rule5)) -> rule1) ((((triple5 ((triple5) -> rule6)) -> rule3)) -> rule5)) -> rule4))] Erin is young.[(((triple7 ((((triple7 ((triple7) -> rule6)) -> rule3)) -> rule5)) -> rule1))] @5: Anne is blue.[(((((triple1 ((((triple1 ((triple1) -> rule6)) -> rule3)) -> rule5)) -> rule1) ((((triple1 ((triple1) -> rule6)) -> rule3)) -> rule5)) -> rule4))] Erin is blue.[(((((triple7 ((((triple7 ((triple7) -> rule6)) -> rule3)) -> rule5)) -> rule1) ((((triple7 ((triple7) -> rule6)) -> rule3)) -> rule5)) -> rule4))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple4 triple3) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
((triple2) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
((triple5 ((((triple5 ((triple5) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple5) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple7) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple5 ((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((triple7 ((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1 ((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple5 ((triple5) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
((((triple7 ((triple7) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
((triple1 ((((triple1 ((triple1) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple6 ((((triple5 ((triple5) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
((((triple5 ((((triple5 ((triple5) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((((triple5 ((triple5) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
int5
Erin is young.
("Erin" "is" "young" "+")
((triple7 ((((triple7 ((triple7) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1 ((((triple1 ((triple1) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((((triple1 ((triple1) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
int5
Erin is blue.
("Erin" "is" "blue" "+")
((((triple7 ((((triple7 ((triple7) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((((triple7 ((triple7) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5