Dave is green. Dave is round. Dave is young. Erin is big. Erin is not blue. Erin is young. Fiona is big. If something is cold then it is not blue. If Dave is not big then Dave is cold. All big things are cold.
Dave is green.
("Dave" "is" "green" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is young.
("Erin" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
If something is cold then it is not blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "-"))
If Dave is not big then Dave is cold.
((("Dave" "is" "big" "~")) -> ("Dave" "is" "cold" "+"))
All big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
Erin is big.
True
1
proof
[(triple4)]
("Erin" "is" "big" "+")
triple4
Dave is not young.
False
1
inv-proof
[(triple3)]
("Dave" "is" "young" "-")
triple3
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "cold" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Dave is green.[(triple1)] Dave is round.[(triple2)] Dave is young.[(triple3)] Erin is big.[(triple4)] Erin is not blue.[(triple5 OR ((((triple4) -> rule3)) -> rule1))] Erin is young.[(triple6)] Fiona is big.[(triple7)] @1: Erin is cold.[(((triple4) -> rule3))] Fiona is cold.[(((triple7) -> rule3))] @2: Fiona is not blue.[(((((triple7) -> rule3)) -> rule1))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Erin is not blue.
("Erin" "is" "blue" "-")
triple5
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple6
Fiona is big.
("Fiona" "is" "big" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
((triple4) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple7) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is not blue.
("Fiona" "is" "blue" "-")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is not blue.
("Fiona" "is" "blue" "-")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2