Charlie is blue. Charlie is cold. Charlie is furry. Charlie is green. Charlie is kind. Charlie is smart. Dave is blue. Dave is kind. Fiona is blue. Fiona is green. Fiona is quiet. Gary is kind. If Charlie is blue then Charlie is kind. All smart, quiet things are green. If Fiona is kind and Fiona is furry then Fiona is cold. Quiet, blue things are furry. Blue things are quiet. If Gary is kind then Gary is blue. Cold things are furry. All blue, furry things are smart.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If Charlie is blue then Charlie is kind.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "kind" "+"))
All smart, quiet things are green.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If Fiona is kind and Fiona is furry then Fiona is cold.
((("Fiona" "is" "kind" "+") ("Fiona" "is" "furry" "+")) -> ("Fiona" "is" "cold" "+"))
Quiet, blue things are furry.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
Blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If Gary is kind then Gary is blue.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "blue" "+"))
Cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
All blue, furry things are smart.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Gary is kind.
True
1
proof
[(triple12)]
("Gary" "is" "kind" "+")
triple12
Charlie is not green.
False
1
inv-proof
[(triple4 OR ((triple6 ((triple1) -> rule5)) -> rule2) OR ((((triple1 triple3) -> rule8) ((triple1) -> rule5)) -> rule2) OR ((((triple1 ((triple2) -> rule7)) -> rule8) ((triple1) -> rule5)) -> rule2) OR ((((triple1 ((((triple1) -> rule5) triple1) -> rule4)) -> rule8) ((triple1) -> rule5)) -> rule2))]
("Charlie" "is" "green" "-")
triple4
((triple6 ((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple1 triple3) -> (rule8 % int3)) ((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((triple1 ((triple2) -> (rule7 % int4))) -> (rule8 % int3)) ((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
((((triple1 ((((triple1) -> (rule5 % int4)) triple1) -> (rule4 % int3))) -> (rule8 % int2)) ((triple1) -> (rule5 % int4))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Gary is blue.
True
2
proof
[(((triple12) -> rule6))]
("Gary" "is" "blue" "+")
((triple12) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple1) -> rule5))]
("Charlie" "is" "quiet" "-")
((triple1) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Dave is furry.
True
4
proof
[(((((triple7) -> rule5) triple7) -> rule4))]
("Dave" "is" "furry" "+")
((((triple7) -> (rule5 % int2)) triple7) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Gary is not quiet.
False
3
inv-proof
[(((((triple12) -> rule6)) -> rule5))]
("Gary" "is" "quiet" "-")
((((triple12) -> (rule6 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Dave is smart.
True
6
proof
[(((triple7 ((((triple7) -> rule5) triple7) -> rule4)) -> rule8))]
("Dave" "is" "smart" "+")
((triple7 ((((triple7) -> (rule5 % int3)) triple7) -> (rule4 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is not smart.
False
6
inv-proof
[(((triple7 ((((triple7) -> rule5) triple7) -> rule4)) -> rule8))]
("Dave" "is" "smart" "-")
((triple7 ((((triple7) -> (rule5 % int3)) triple7) -> (rule4 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Gary is smart.
True
9
proof
[(((((triple12) -> rule6) ((((((triple12) -> rule6)) -> rule5) ((triple12) -> rule6)) -> rule4)) -> rule8))]
("Gary" "is" "smart" "+")
((((triple12) -> (rule6 % int4)) ((((((triple12) -> (rule6 % int4))) -> (rule5 % int3)) ((triple12) -> (rule6 % int4))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Dave is not green.
False
9
inv-proof
[(((((triple7 ((((triple7) -> rule5) triple7) -> rule4)) -> rule8) ((triple7) -> rule5)) -> rule2))]
("Dave" "is" "green" "-")
((((triple7 ((((triple7) -> (rule5 % int4)) triple7) -> (rule4 % int3))) -> (rule8 % int2)) ((triple7) -> (rule5 % int4))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Gary is green.
True
13
proof
[(((((((triple12) -> rule6) ((((((triple12) -> rule6)) -> rule5) ((triple12) -> rule6)) -> rule4)) -> rule8) ((((triple12) -> rule6)) -> rule5)) -> rule2))]
("Gary" "is" "green" "+")
((((((triple12) -> (rule6 % int5)) ((((((triple12) -> (rule6 % int5))) -> (rule5 % int4)) ((triple12) -> (rule6 % int5))) -> (rule4 % int3))) -> (rule8 % int2)) ((((triple12) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is blue.
("Gary" "is" "blue" "+")
int5
Gary is not green.
False
13
inv-proof
[(((((((triple12) -> rule6) ((((((triple12) -> rule6)) -> rule5) ((triple12) -> rule6)) -> rule4)) -> rule8) ((((triple12) -> rule6)) -> rule5)) -> rule2))]
("Gary" "is" "green" "-")
((((((triple12) -> (rule6 % int5)) ((((((triple12) -> (rule6 % int5))) -> (rule5 % int4)) ((triple12) -> (rule6 % int5))) -> (rule4 % int3))) -> (rule8 % int2)) ((((triple12) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is blue.
("Gary" "is" "blue" "+")
int5
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "cold" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2)] Charlie is furry.[(triple3 OR ((triple2) -> rule7) OR ((((triple1) -> rule5) triple1) -> rule4))] Charlie is green.[(triple4 OR ((triple6 ((triple1) -> rule5)) -> rule2) OR ((((triple1 triple3) -> rule8) ((triple1) -> rule5)) -> rule2) OR ((((triple1 ((triple2) -> rule7)) -> rule8) ((triple1) -> rule5)) -> rule2) OR ((((triple1 ((((triple1) -> rule5) triple1) -> rule4)) -> rule8) ((triple1) -> rule5)) -> rule2))] Charlie is kind.[(triple5 OR ((triple1) -> rule1))] Charlie is smart.[(triple6 OR ((triple1 triple3) -> rule8) OR ((triple1 ((triple2) -> rule7)) -> rule8) OR ((triple1 ((((triple1) -> rule5) triple1) -> rule4)) -> rule8))] Dave is blue.[(triple7)] Dave is kind.[(triple8)] Fiona is blue.[(triple9)] Fiona is green.[(triple10 OR ((((triple9 ((triple11 triple9) -> rule4)) -> rule8) triple11) -> rule2) OR ((((triple9 ((triple11 triple9) -> rule4)) -> rule8) ((triple9) -> rule5)) -> rule2) OR ((((triple9 ((((triple9) -> rule5) triple9) -> rule4)) -> rule8) triple11) -> rule2) OR ((((triple9 ((((triple9) -> rule5) triple9) -> rule4)) -> rule8) ((triple9) -> rule5)) -> rule2))] Fiona is quiet.[(triple11 OR ((triple9) -> rule5))] Gary is kind.[(triple12)] @1: Charlie is quiet.[(((triple1) -> rule5))] Dave is quiet.[(((triple7) -> rule5))] Fiona is furry.[(((triple11 triple9) -> rule4) OR ((((triple9) -> rule5) triple9) -> rule4))] Gary is blue.[(((triple12) -> rule6))] @2: Dave is furry.[(((((triple7) -> rule5) triple7) -> rule4))] Fiona is smart.[(((triple9 ((triple11 triple9) -> rule4)) -> rule8) OR ((triple9 ((((triple9) -> rule5) triple9) -> rule4)) -> rule8))] Gary is quiet.[(((((triple12) -> rule6)) -> rule5))] @3: Dave is smart.[(((triple7 ((((triple7) -> rule5) triple7) -> rule4)) -> rule8))] Gary is furry.[(((((((triple12) -> rule6)) -> rule5) ((triple12) -> rule6)) -> rule4))] @4: Dave is green.[(((((triple7 ((((triple7) -> rule5) triple7) -> rule4)) -> rule8) ((triple7) -> rule5)) -> rule2))] Gary is smart.[(((((triple12) -> rule6) ((((((triple12) -> rule6)) -> rule5) ((triple12) -> rule6)) -> rule4)) -> rule8))] @5: Gary is green.[(((((((triple12) -> rule6) ((((((triple12) -> rule6)) -> rule5) ((triple12) -> rule6)) -> rule4)) -> rule8) ((((triple12) -> rule6)) -> rule5)) -> rule2))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
((triple2) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple1) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple4
((triple6 ((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple1 triple3) -> (rule8 % int3)) ((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((triple1 ((triple2) -> (rule7 % int4))) -> (rule8 % int3)) ((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
((((triple1 ((((triple1) -> (rule5 % int4)) triple1) -> (rule4 % int3))) -> (rule8 % int2)) ((triple1) -> (rule5 % int4))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
((triple1) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
((triple1 triple3) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple1 ((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((triple1 ((((triple1) -> (rule5 % int3)) triple1) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
triple7
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
Fiona is green.
("Fiona" "is" "green" "+")
triple10
((((triple9 ((triple11 triple9) -> (rule4 % int3))) -> (rule8 % int2)) triple11) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((((triple9 ((triple11 triple9) -> (rule4 % int4))) -> (rule8 % int3)) ((triple9) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
int4
((((triple9 ((((triple9) -> (rule5 % int4)) triple9) -> (rule4 % int3))) -> (rule8 % int2)) triple11) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
((((triple9 ((((triple9) -> (rule5 % int4)) triple9) -> (rule4 % int3))) -> (rule8 % int2)) ((triple9) -> (rule5 % int4))) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple11
((triple9) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple12
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple7) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple11 triple9) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple9) -> (rule5 % int2)) triple9) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((triple12) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple7) -> (rule5 % int2)) triple7) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple9 ((triple11 triple9) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((triple9 ((((triple9) -> (rule5 % int3)) triple9) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple12) -> (rule6 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((triple7 ((((triple7) -> (rule5 % int3)) triple7) -> (rule4 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
((((((triple12) -> (rule6 % int3))) -> (rule5 % int2)) ((triple12) -> (rule6 % int3))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
((((triple7 ((((triple7) -> (rule5 % int4)) triple7) -> (rule4 % int3))) -> (rule8 % int2)) ((triple7) -> (rule5 % int4))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
((((triple12) -> (rule6 % int4)) ((((((triple12) -> (rule6 % int4))) -> (rule5 % int3)) ((triple12) -> (rule6 % int4))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is green.
("Gary" "is" "green" "+")
((((((triple12) -> (rule6 % int5)) ((((((triple12) -> (rule6 % int5))) -> (rule5 % int4)) ((triple12) -> (rule6 % int5))) -> (rule4 % int3))) -> (rule8 % int2)) ((((triple12) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is blue.
("Gary" "is" "blue" "+")
int5