Anne is nice. Dave is big. Fiona is white. Gary is red. If something is red then it is big. All big things are cold.
Anne is nice.
("Anne" "is" "nice" "+")
Dave is big.
("Dave" "is" "big" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is red.
("Gary" "is" "red" "+")
If something is red then it is big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
All big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
Anne is nice.
True
1
proof
[(triple1)]
("Anne" "is" "nice" "+")
triple1
Gary is not red.
False
1
inv-proof
[(triple4)]
("Gary" "is" "red" "-")
triple4
Gary is big.
True
2
proof
[(((triple4) -> rule1))]
("Gary" "is" "big" "+")
((triple4) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not big.
False
2
inv-proof
[(((triple4) -> rule1))]
("Gary" "is" "big" "-")
((triple4) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
True
3
proof
[(((((triple4) -> rule1)) -> rule2))]
("Gary" "is" "cold" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not cold.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule2))]
("Gary" "is" "cold" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Anne is not cold.
Unknown
inv-rconc
[@2: Anne is cold.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Anne" "is" "cold" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "big" "+")
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "big" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Anne is nice.[(triple1)] Dave is big.[(triple2)] Fiona is white.[(triple3)] Gary is red.[(triple4)] @1: Dave is cold.[(((triple2) -> rule2))] Gary is big.[(((triple4) -> rule1))] @2: Gary is cold.[(((((triple4) -> rule1)) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Fiona is white.
("Fiona" "is" "white" "+")
triple3
Gary is red.
("Gary" "is" "red" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple4) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2