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