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