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