Charlie is cold. Charlie is furry. Charlie is not nice. Charlie is red. Charlie is smart. Charlie is not white. Dave is not blue. Dave is not red. Dave is white. Fiona is white. If Fiona is blue and Fiona is nice then Fiona is cold. If Fiona is cold then Fiona is red. If someone is white then they are cold. If Fiona is red then Fiona is not furry. If Dave is cold and Dave is not white then Dave is not nice. If Charlie is not blue and Charlie is not cold then Charlie is furry.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is not red.
("Dave" "is" "red" "-")
Dave is white.
("Dave" "is" "white" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If Fiona is blue and Fiona is nice then Fiona is cold.
((("Fiona" "is" "blue" "+") ("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "cold" "+"))
If Fiona is cold then Fiona is red.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "red" "+"))
If someone is white then they are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If Fiona is red then Fiona is not furry.
((("Fiona" "is" "red" "+")) -> ("Fiona" "is" "furry" "-"))
If Dave is cold and Dave is not white then Dave is not nice.
((("Dave" "is" "cold" "+") ("Dave" "is" "white" "~")) -> ("Dave" "is" "nice" "-"))
If Charlie is not blue and Charlie is not cold then Charlie is furry.
((("Charlie" "is" "blue" "~") ("Charlie" "is" "cold" "~")) -> ("Charlie" "is" "furry" "+"))
Charlie is red.
True
1
proof
[(triple4)]
("Charlie" "is" "red" "+")
triple4
Charlie is not cold.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "cold" "-")
triple1
Dave is cold.
True
2
proof
[(((triple9) -> rule3))]
("Dave" "is" "cold" "+")
((triple9) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple9) -> rule3))]
("Dave" "is" "cold" "-")
((triple9) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Fiona is red.
True
3
proof
[(((((triple10) -> rule3)) -> rule2))]
("Fiona" "is" "red" "+")
((((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not red.
False
3
inv-proof
[(((((triple10) -> rule3)) -> rule2))]
("Fiona" "is" "red" "-")
((((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not furry.
True
4
proof
[(((((((triple10) -> rule3)) -> rule2)) -> rule4))]
("Fiona" "is" "furry" "-")
((((((triple10) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is furry.
False
4
inv-proof
[(((((((triple10) -> rule3)) -> rule2)) -> rule4))]
("Fiona" "is" "furry" "+")
((((((triple10) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Charlie is cold.[(triple1)] Charlie is furry.[(triple2)] Charlie is not nice.[(triple3)] Charlie is not white.[(triple6)] Charlie is red.[(triple4)] Charlie is smart.[(triple5)] Dave is not blue.[(triple7)] Dave is not red.[(triple8)] Dave is white.[(triple9)] Fiona is white.[(triple10)] @1: Dave is cold.[(((triple9) -> rule3))] Fiona is cold.[(((triple10) -> rule3))] @2: Fiona is red.[(((((triple10) -> rule3)) -> rule2))] @3: Fiona is not furry.[(((((((triple10) -> rule3)) -> rule2)) -> rule4))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple3
Charlie is not white.
("Charlie" "is" "white" "-")
triple6
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Dave is not blue.
("Dave" "is" "blue" "-")
triple7
Dave is not red.
("Dave" "is" "red" "-")
triple8
Dave is white.
("Dave" "is" "white" "+")
triple9
Fiona is white.
("Fiona" "is" "white" "+")
triple10
Dave is cold.
("Dave" "is" "cold" "+")
((triple9) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple10) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not furry.
("Fiona" "is" "furry" "-")
((((((triple10) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3