Dave is blue. Dave is cold. Dave is nice. Dave is quiet. Dave is not round. Fiona is big. Fiona is blue. Fiona is cold. Fiona is not nice. Fiona is not quiet. Fiona is round. Fiona is not young. Gary is big. Gary is cold. Gary is round. Gary is not young. Quiet, nice things are cold. If something is blue and not round then it is cold. Quiet, nice things are cold. Big things are cold. All blue, nice things are young. Nice things are big.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not round.
("Dave" "is" "round" "-")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is not nice.
("Fiona" "is" "nice" "-")
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is not young.
("Fiona" "is" "young" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is not young.
("Gary" "is" "young" "-")
Quiet, nice things are cold.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is blue and not round then it is cold.
((("something" "is" "blue" "+") ("something" "is" "round" "~")) -> ("something" "is" "cold" "+"))
Quiet, nice things are cold.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
All blue, nice things are young.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
Nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Dave is not round.
True
1
proof
[(triple5)]
("Dave" "is" "round" "-")
triple5
Fiona is not blue.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "blue" "-")
triple7
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Dave is blue.[(triple1)] Dave is cold.[(triple2 OR ((triple1 triple5) -> rule2) OR ((triple4 triple3) -> rule1) OR ((triple4 triple3) -> rule3) OR ((((triple3) -> rule6)) -> rule4))] Dave is nice.[(triple3)] Dave is not round.[(triple5)] Dave is quiet.[(triple4)] Fiona is big.[(triple6)] Fiona is blue.[(triple7)] Fiona is cold.[(triple8 OR ((triple6) -> rule4))] Fiona is not nice.[(triple9)] Fiona is not quiet.[(triple10)] Fiona is not young.[(triple12)] Fiona is round.[(triple11)] Gary is big.[(triple13)] Gary is cold.[(triple14 OR ((triple13) -> rule4))] Gary is not young.[(triple16)] Gary is round.[(triple15)] @1: Dave is big.[(((triple3) -> rule6))] Dave is young.[(((triple1 triple3) -> rule5))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
((triple1 triple5) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple4 triple3) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple4 triple3) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is not round.
("Dave" "is" "round" "-")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
triple6
Fiona is blue.
("Fiona" "is" "blue" "+")
triple7
Fiona is cold.
("Fiona" "is" "cold" "+")
triple8
((triple6) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is not nice.
("Fiona" "is" "nice" "-")
triple9
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
triple10
Fiona is not young.
("Fiona" "is" "young" "-")
triple12
Fiona is round.
("Fiona" "is" "round" "+")
triple11
Gary is big.
("Gary" "is" "big" "+")
triple13
Gary is cold.
("Gary" "is" "cold" "+")
triple14
((triple13) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not young.
("Gary" "is" "young" "-")
triple16
Gary is round.
("Gary" "is" "round" "+")
triple15
Dave is big.
("Dave" "is" "big" "+")
((triple3) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple1 triple3) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1