Dave is blue. Dave is cold. Dave is nice. Dave is red. Dave is rough. Dave is round. Dave is young. Erin is rough. Erin is round. Erin is young. Harry is red. Harry is rough. If someone is rough and not red then they are cold. If someone is blue and not red then they are cold. All young people are cold. All red people are young. If Harry is cold then Harry is blue. If someone is rough and not red then they are not nice.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is rough and not red then they are cold.
((("someone" "is" "rough" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "cold" "+"))
If someone is blue and not red then they are cold.
((("someone" "is" "blue" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "cold" "+"))
All young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
All red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If Harry is cold then Harry is blue.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "blue" "+"))
If someone is rough and not red then they are not nice.
((("someone" "is" "rough" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "nice" "-"))
Dave is round.
True
1
proof
[(triple6)]
("Dave" "is" "round" "+")
triple6
Dave is not nice.
False
1
inv-proof
[(triple3)]
("Dave" "is" "nice" "-")
triple3
Harry is young.
True
2
proof
[(((triple11) -> rule4))]
("Harry" "is" "young" "+")
((triple11) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Erin is not cold.
False
2
inv-proof
[(((triple10) -> rule3))]
("Erin" "is" "cold" "-")
((triple10) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Harry is cold.
True
3
proof
[(((((triple11) -> rule4)) -> rule3))]
("Harry" "is" "cold" "+")
((((triple11) -> (rule4 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not cold.
False
3
inv-proof
[(((((triple11) -> rule4)) -> rule3))]
("Harry" "is" "cold" "-")
((((triple11) -> (rule4 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is blue.
True
4
proof
[(((((((triple11) -> rule4)) -> rule3)) -> rule5))]
("Harry" "is" "blue" "+")
((((((triple11) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not blue.
False
4
inv-proof
[(((((((triple11) -> rule4)) -> rule3)) -> rule5))]
("Harry" "is" "blue" "-")
((((((triple11) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Dave is blue.[(triple1)] Dave is cold.[(triple2 OR ((triple7) -> rule3) OR ((((triple4) -> rule4)) -> rule3))] Dave is nice.[(triple3)] Dave is red.[(triple4)] Dave is rough.[(triple5)] Dave is round.[(triple6)] Dave is young.[(triple7 OR ((triple4) -> rule4))] Erin is rough.[(triple8)] Erin is round.[(triple9)] Erin is young.[(triple10)] Harry is red.[(triple11)] Harry is rough.[(triple12)] @1: Erin is cold.[(((triple10) -> rule3))] Harry is young.[(((triple11) -> rule4))] @2: Harry is cold.[(((((triple11) -> rule4)) -> rule3))] @3: Harry is blue.[(((((((triple11) -> rule4)) -> rule3)) -> rule5))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
((triple7) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
((triple4) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple8
Erin is round.
("Erin" "is" "round" "+")
triple9
Erin is young.
("Erin" "is" "young" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Erin is cold.
("Erin" "is" "cold" "+")
((triple10) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple11) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((((triple11) -> (rule4 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((((triple11) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3