Dave is green. Fiona is red. Gary is green. Quiet, red things are furry. Red, cold things are quiet. All green, white things are furry. If Gary is furry then Gary is red. If something is kind then it is cold. All green things are white. If something is green and furry then it is kind. If Dave is red then Dave is green.
Dave is green.
("Dave" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is green.
("Gary" "is" "green" "+")
Quiet, red things are furry.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Red, cold things are quiet.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
All green, white things are furry.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If Gary is furry then Gary is red.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "red" "+"))
If something is kind then it is cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
All green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is green and furry then it is kind.
((("something" "is" "green" "+") ("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
If Dave is red then Dave is green.
((("Dave" "is" "red" "+")) -> ("Dave" "is" "green" "+"))
Gary is green.
True
1
proof
[(triple3)]
("Gary" "is" "green" "+")
triple3
Fiona is not red.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "red" "-")
triple2
Dave is white.
True
2
proof
[(((triple1) -> rule6))]
("Dave" "is" "white" "+")
((triple1) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple3) -> rule6))]
("Gary" "is" "white" "-")
((triple3) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "white" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "quiet" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Dave is green.[(triple1)] Fiona is red.[(triple2)] Gary is green.[(triple3)] @1: Dave is white.[(((triple1) -> rule6))] Gary is white.[(((triple3) -> rule6))] @2: Dave is furry.[(((triple1 ((triple1) -> rule6)) -> rule3))] Gary is furry.[(((triple3 ((triple3) -> rule6)) -> rule3))] @3: Dave is kind.[(((triple1 ((triple1 ((triple1) -> rule6)) -> rule3)) -> rule7))] Gary is kind.[(((triple3 ((triple3 ((triple3) -> rule6)) -> rule3)) -> rule7))] Gary is red.[(((((triple3 ((triple3) -> rule6)) -> rule3)) -> rule4))] @4: Dave is cold.[(((((triple1 ((triple1 ((triple1) -> rule6)) -> rule3)) -> rule7)) -> rule5))] Gary is cold.[(((((triple3 ((triple3 ((triple3) -> rule6)) -> rule3)) -> rule7)) -> rule5))] @5: Gary is quiet.[(((((((triple3 ((triple3) -> rule6)) -> rule3)) -> rule4) ((((triple3 ((triple3 ((triple3) -> rule6)) -> rule3)) -> rule7)) -> rule5)) -> rule2))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Fiona is red.
("Fiona" "is" "red" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
((triple1) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple3) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((triple3 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((triple1 ((triple1 ((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
((triple3 ((triple3 ((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((((triple3 ((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
((((triple1 ((triple1 ((triple1) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
((((triple3 ((triple3 ((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((triple3 ((triple3) -> (rule6 % int6))) -> (rule3 % int5))) -> (rule4 % int4)) ((((triple3 ((triple3 ((triple3) -> (rule6 % int6))) -> (rule3 % int5))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is furry.
("Gary" "is" "furry" "+")
int5
Gary is white.
("Gary" "is" "white" "+")
int6