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