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