Dave is big. Dave is furry. Dave is not green. Dave is kind. Dave is red. Dave is smart. Dave is white. Fiona is furry. Fiona is green. Fiona is red. Fiona is smart. Gary is big. Gary is not furry. Gary is green. Gary is smart. Gary is white. All green things are white. If something is big and not kind then it is white. If something is smart then it is white. Green, kind things are white. All white things are big. White things are red. If Gary is not green then Gary is red. If Dave is white then Dave is red.
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is green.
("Gary" "is" "green" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
All green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is big and not kind then it is white.
((("something" "is" "big" "+") ("something" "is" "kind" "~")) -> ("something" "is" "white" "+"))
If something is smart then it is white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
Green, kind things are white.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
All white things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
White things are red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
If Gary is not green then Gary is red.
((("Gary" "is" "green" "~")) -> ("Gary" "is" "red" "+"))
If Dave is white then Dave is red.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "red" "+"))
Dave is red.
True
1
proof
[(triple5 OR ((triple7) -> rule6) OR ((triple7) -> rule8) OR ((((triple6) -> rule3)) -> rule6) OR ((((triple6) -> rule3)) -> rule8))]
("Dave" "is" "red" "+")
triple5
((triple7) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple7) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple6) -> (rule3 % int2))) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Gary is not green.
False
1
inv-proof
[(triple14)]
("Gary" "is" "green" "-")
triple14
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Dave is big.[(triple1 OR ((triple7) -> rule5) OR ((((triple6) -> rule3)) -> rule5))] Dave is furry.[(triple2)] Dave is kind.[(triple4)] Dave is not green.[(triple3)] Dave is red.[(triple5 OR ((triple7) -> rule6) OR ((triple7) -> rule8) OR ((((triple6) -> rule3)) -> rule6) OR ((((triple6) -> rule3)) -> rule8))] Dave is smart.[(triple6)] Dave is white.[(triple7 OR ((triple6) -> rule3))] Fiona is furry.[(triple8)] Fiona is green.[(triple9)] Fiona is red.[(triple10 OR ((((triple11) -> rule3)) -> rule6) OR ((((triple9) -> rule1)) -> rule6))] Fiona is smart.[(triple11)] Gary is big.[(triple12 OR ((triple16) -> rule5) OR ((((triple14) -> rule1)) -> rule5) OR ((((triple15) -> rule3)) -> rule5))] Gary is green.[(triple14)] Gary is not furry.[(triple13)] Gary is smart.[(triple15)] Gary is white.[(triple16 OR ((triple14) -> rule1) OR ((triple15) -> rule3))] @1: Fiona is white.[(((triple11) -> rule3) OR ((triple9) -> rule1))] Gary is red.[(((triple16) -> rule6) OR ((((triple14) -> rule1)) -> rule6) OR ((((triple15) -> rule3)) -> rule6))] @2: Fiona is big.[(((((triple11) -> rule3)) -> rule5) OR ((((triple9) -> rule1)) -> rule5))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple7) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is not green.
("Dave" "is" "green" "-")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple5
((triple7) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple7) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple6) -> (rule3 % int2))) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
((triple6) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple8
Fiona is green.
("Fiona" "is" "green" "+")
triple9
Fiona is red.
("Fiona" "is" "red" "+")
triple10
((((triple11) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((((triple9) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple11
Gary is big.
("Gary" "is" "big" "+")
triple12
((triple16) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple14) -> (rule1 % int2))) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((triple15) -> (rule3 % int2))) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple14
Gary is not furry.
("Gary" "is" "furry" "-")
triple13
Gary is smart.
("Gary" "is" "smart" "+")
triple15
Gary is white.
("Gary" "is" "white" "+")
triple16
((triple14) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple15) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple11) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((triple9) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple16) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple14) -> (rule1 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((triple15) -> (rule3 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
((((triple11) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((((triple9) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2