Dave is blue. Dave is cold. Dave is nice. Dave is white. Erin is blue. Erin is nice. Erin is red. Erin is white. Fiona is blue. Fiona is round. If Dave is white and Dave is cold then Dave is red. If Dave is round then Dave is red. All white, red things are blue. Round things are blue. Round things are blue. If something is rough and nice then it is cold.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is round.
("Fiona" "is" "round" "+")
If Dave is white and Dave is cold then Dave is red.
((("Dave" "is" "white" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "red" "+"))
If Dave is round then Dave is red.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "red" "+"))
All white, red things are blue.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If something is rough and nice then it is cold.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Erin is blue.
True
1
proof
[(triple5 OR ((triple8 triple7) -> rule3))]
("Erin" "is" "blue" "+")
triple5
((triple8 triple7) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Fiona is not round.
False
1
inv-proof
[(triple10)]
("Fiona" "is" "round" "-")
triple10
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "cold" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Dave is blue.[(triple1 OR ((triple4 ((triple4 triple2) -> rule1)) -> rule3))] Dave is cold.[(triple2)] Dave is nice.[(triple3)] Dave is white.[(triple4)] Erin is blue.[(triple5 OR ((triple8 triple7) -> rule3))] Erin is nice.[(triple6)] Erin is red.[(triple7)] Erin is white.[(triple8)] Fiona is blue.[(triple9 OR ((triple10) -> rule4) OR ((triple10) -> rule5))] Fiona is round.[(triple10)] @1: Dave is red.[(((triple4 triple2) -> rule1))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((triple4 ((triple4 triple2) -> (rule1 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
((triple8 triple7) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple6
Erin is red.
("Erin" "is" "red" "+")
triple7
Erin is white.
("Erin" "is" "white" "+")
triple8
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
((triple10) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple10) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
triple10
Dave is red.
("Dave" "is" "red" "+")
((triple4 triple2) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1