Dave is green. Dave is round. Dave is smart. Fiona is blue. Fiona is kind. Fiona is young. Harry is blue. Harry is green. Harry is kind. Harry is young. If Harry is cold and Harry is round then Harry is kind. If something is young then it is cold. If something is round then it is blue. All young, kind things are round. If something is smart then it is young. If something is blue then it is cold.
Dave is green.
("Dave" "is" "green" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is cold and Harry is round then Harry is kind.
((("Harry" "is" "cold" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "kind" "+"))
If something is young then it is cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If something is round then it is blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
All young, kind things are round.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If something is smart then it is young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If something is blue then it is cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Dave is green.
True
1
proof
[(triple1)]
("Dave" "is" "green" "+")
triple1
Dave is not green.
False
1
inv-proof
[(triple1)]
("Dave" "is" "green" "-")
triple1
Fiona is cold.
True
2
proof
[(((triple4) -> rule6) OR ((triple6) -> rule2) OR ((((((triple6 triple5) -> rule4)) -> rule3)) -> rule6))]
("Fiona" "is" "cold" "+")
((triple4) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple6) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((((triple6 triple5) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Harry is not cold.
False
2
inv-proof
[(((triple10) -> rule2) OR ((triple7) -> rule6) OR ((((((triple10 triple9) -> rule4)) -> rule3)) -> rule6))]
("Harry" "is" "cold" "-")
((triple10) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple7) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((((triple10 triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Dave is green.[(triple1)] Dave is round.[(triple2)] Dave is smart.[(triple3)] Fiona is blue.[(triple4 OR ((((triple6 triple5) -> rule4)) -> rule3))] Fiona is kind.[(triple5)] Fiona is young.[(triple6)] Harry is blue.[(triple7 OR ((((triple10 triple9) -> rule4)) -> rule3))] Harry is green.[(triple8)] Harry is kind.[(triple9)] Harry is young.[(triple10)] @1: Dave is blue.[(((triple2) -> rule3))] Dave is young.[(((triple3) -> rule5))] Fiona is cold.[(((triple4) -> rule6) OR ((triple6) -> rule2) OR ((((((triple6 triple5) -> rule4)) -> rule3)) -> rule6))] Fiona is round.[(((triple6 triple5) -> rule4))] Harry is cold.[(((triple10) -> rule2) OR ((triple7) -> rule6) OR ((((((triple10 triple9) -> rule4)) -> rule3)) -> rule6))] Harry is round.[(((triple10 triple9) -> rule4))] @2: Dave is cold.[(((((triple2) -> rule3)) -> rule6) OR ((((triple3) -> rule5)) -> rule2))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Fiona is blue.
("Fiona" "is" "blue" "+")
triple4
((((triple6 triple5) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple5
Fiona is young.
("Fiona" "is" "young" "+")
triple6
Harry is blue.
("Harry" "is" "blue" "+")
triple7
((((triple10 triple9) -> (rule4 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Dave is blue.
("Dave" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple3) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple4) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple6) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((((triple6 triple5) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
((triple6 triple5) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple10) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple7) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((((triple10 triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
((triple10 triple9) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2