Bob is young. Dave is red. Erin is nice. Erin is quiet. Erin is not red. Erin is young. Gary is young. If Dave is blue and Dave is nice then Dave is red. If Erin is blue then Erin is nice. Young, red things are not quiet. Young things are cold. If something is nice and not quiet then it is cold. All nice, blue things are cold. All nice, blue things are cold. If something is nice then it is cold.
Bob is young.
("Bob" "is" "young" "+")
Dave is red.
("Dave" "is" "red" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is not red.
("Erin" "is" "red" "-")
Erin is young.
("Erin" "is" "young" "+")
Gary is young.
("Gary" "is" "young" "+")
If Dave is blue and Dave is nice then Dave is red.
((("Dave" "is" "blue" "+") ("Dave" "is" "nice" "+")) -> ("Dave" "is" "red" "+"))
If Erin is blue then Erin is nice.
((("Erin" "is" "blue" "+")) -> ("Erin" "is" "nice" "+"))
Young, red things are not quiet.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "-"))
Young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If something is nice and not quiet then it is cold.
((("something" "is" "nice" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "cold" "+"))
All nice, blue things are cold.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
All nice, blue things are cold.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If something is nice then it is cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Bob is young.
True
1
proof
[(triple1)]
("Bob" "is" "young" "+")
triple1
Dave is not red.
False
1
inv-proof
[(triple2)]
("Dave" "is" "red" "-")
triple2
Bob is cold.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Erin is not cold.
False
2
inv-proof
[(((triple3) -> rule8) OR ((triple6) -> rule4))]
("Erin" "is" "cold" "-")
((triple3) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple6) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Bob is young.[(triple1)] Dave is red.[(triple2)] Erin is nice.[(triple3)] Erin is not red.[(triple5)] Erin is quiet.[(triple4)] Erin is young.[(triple6)] Gary is young.[(triple7)] @1: Bob is cold.[(((triple1) -> rule4))] Erin is cold.[(((triple3) -> rule8) OR ((triple6) -> rule4))] Gary is cold.[(((triple7) -> rule4))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Erin is not red.
("Erin" "is" "red" "-")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple3) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple6) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple7) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1