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