Dave is cold. Dave is red. Erin is white. Fiona is cold. Fiona is quiet. Fiona is not red. Fiona is smart. If Erin is not cold then Erin is smart. If someone is kind and not red then they are not smart. All white people are smart. Cold, red people are smart. All smart people are blue. If someone is quiet and cold then they are white. Red, kind people are white. Blue, cold people are white.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is not red.
("Fiona" "is" "red" "-")
Fiona is smart.
("Fiona" "is" "smart" "+")
If Erin is not cold then Erin is smart.
((("Erin" "is" "cold" "~")) -> ("Erin" "is" "smart" "+"))
If someone is kind and not red then they are not smart.
((("someone" "is" "kind" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "smart" "-"))
All white people are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
Cold, red people are smart.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
All smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet and cold then they are white.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
Red, kind people are white.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Blue, cold people are white.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
Dave is red.
True
1
proof
[(triple2)]
("Dave" "is" "red" "+")
triple2
Fiona is not smart.
False
1
inv-proof
[(triple7 OR ((((triple5 triple4) -> rule6)) -> rule3))]
("Fiona" "is" "smart" "-")
triple7
((((triple5 triple4) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Erin is smart.
True
2
proof
[(((triple3) -> rule3))]
("Erin" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Fiona is not white.
False
3
inv-proof
[(((triple5 triple4) -> rule6) OR ((((triple7) -> rule5) triple4) -> rule8))]
("Fiona" "is" "white" "-")
((triple5 triple4) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple7) -> (rule5 % int2)) triple4) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Erin is blue.
True
3
proof
[(((((triple3) -> rule3)) -> rule5))]
("Erin" "is" "blue" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not blue.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule5))]
("Erin" "is" "blue" "-")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Dave is white.
True
6
proof
[(((((((triple1 triple2) -> rule4)) -> rule5) triple1) -> rule8))]
("Dave" "is" "white" "+")
((((((triple1 triple2) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is not white.
False
6
inv-proof
[(((((((triple1 triple2) -> rule4)) -> rule5) triple1) -> rule8))]
("Dave" "is" "white" "-")
((((((triple1 triple2) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Dave is cold.[(triple1)] Dave is red.[(triple2)] Erin is white.[(triple3)] Fiona is cold.[(triple4)] Fiona is not red.[(triple6)] Fiona is quiet.[(triple5)] Fiona is smart.[(triple7 OR ((((triple5 triple4) -> rule6)) -> rule3))] @1: Dave is smart.[(((triple1 triple2) -> rule4))] Erin is smart.[(((triple3) -> rule3))] Fiona is blue.[(((triple7) -> rule5) OR ((((((triple5 triple4) -> rule6)) -> rule3)) -> rule5))] Fiona is white.[(((triple5 triple4) -> rule6) OR ((((triple7) -> rule5) triple4) -> rule8))] @2: Dave is blue.[(((((triple1 triple2) -> rule4)) -> rule5))] Erin is blue.[(((((triple3) -> rule3)) -> rule5))] @3: Dave is white.[(((((((triple1 triple2) -> rule4)) -> rule5) triple1) -> rule8))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple4
Fiona is not red.
("Fiona" "is" "red" "-")
triple6
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple5
Fiona is smart.
("Fiona" "is" "smart" "+")
triple7
((((triple5 triple4) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((triple1 triple2) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple7) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((((((triple5 triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
((triple5 triple4) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple7) -> (rule5 % int2)) triple4) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((((triple1 triple2) -> (rule4 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((((triple1 triple2) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3