Dave is big. Dave is kind. Dave is quiet. Dave is red. Dave is round. Dave is white. Erin is big. Erin is red. Erin is round. Erin is white. Gary is big. Gary is kind. Gary is quiet. Gary is red. Gary is round. If Dave is kind then Dave is cold. If Dave is kind then Dave is white. If Dave is big then Dave is quiet.
Dave is big.
("Dave" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
If Dave is kind then Dave is cold.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "cold" "+"))
If Dave is kind then Dave is white.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "white" "+"))
If Dave is big then Dave is quiet.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "quiet" "+"))
Erin is round.
True
1
proof
[(triple9)]
("Erin" "is" "round" "+")
triple9
Gary is not kind.
False
1
inv-proof
[(triple12)]
("Gary" "is" "kind" "-")
triple12
Dave is cold.
True
2
proof
[(((triple2) -> rule1))]
("Dave" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple2) -> rule1))]
("Dave" "is" "cold" "-")
((triple2) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Dave is big.[(triple1)] Dave is kind.[(triple2)] Dave is quiet.[(triple3 OR ((triple1) -> rule3))] Dave is red.[(triple4)] Dave is round.[(triple5)] Dave is white.[(triple6 OR ((triple2) -> rule2))] Erin is big.[(triple7)] Erin is red.[(triple8)] Erin is round.[(triple9)] Erin is white.[(triple10)] Gary is big.[(triple11)] Gary is kind.[(triple12)] Gary is quiet.[(triple13)] Gary is red.[(triple14)] Gary is round.[(triple15)] @1: Dave is cold.[(((triple2) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
((triple1) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
((triple2) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple7
Erin is red.
("Erin" "is" "red" "+")
triple8
Erin is round.
("Erin" "is" "round" "+")
triple9
Erin is white.
("Erin" "is" "white" "+")
triple10
Gary is big.
("Gary" "is" "big" "+")
triple11
Gary is kind.
("Gary" "is" "kind" "+")
triple12
Gary is quiet.
("Gary" "is" "quiet" "+")
triple13
Gary is red.
("Gary" "is" "red" "+")
triple14
Gary is round.
("Gary" "is" "round" "+")
triple15
Dave is cold.
("Dave" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1