Charlie is cold. Charlie is nice. Charlie is rough. Dave is big. Fiona is cold. Fiona is not kind. Fiona is quiet. Gary is big. Gary is kind. Gary is nice. Gary is not quiet. Gary is rough. If Gary is rough and Gary is kind then Gary is big. If something is big then it is cold. If Fiona is nice and Fiona is white then Fiona is not quiet. If something is rough and not big then it is white. Kind things are not white. If Fiona is white then Fiona is not cold.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is not kind.
("Fiona" "is" "kind" "-")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
Gary is rough.
("Gary" "is" "rough" "+")
If Gary is rough and Gary is kind then Gary is big.
((("Gary" "is" "rough" "+") ("Gary" "is" "kind" "+")) -> ("Gary" "is" "big" "+"))
If something is big then it is cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If Fiona is nice and Fiona is white then Fiona is not quiet.
((("Fiona" "is" "nice" "+") ("Fiona" "is" "white" "+")) -> ("Fiona" "is" "quiet" "-"))
If something is rough and not big then it is white.
((("something" "is" "rough" "+") ("something" "is" "big" "~")) -> ("something" "is" "white" "+"))
Kind things are not white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "-"))
If Fiona is white then Fiona is not cold.
((("Fiona" "is" "white" "+")) -> ("Fiona" "is" "cold" "-"))
Charlie is rough.
True
1
proof
[(triple3)]
("Charlie" "is" "rough" "+")
triple3
Fiona is not cold.
False
1
inv-proof
[(triple5)]
("Fiona" "is" "cold" "-")
triple5
Gary is not white.
True
2
proof
[(((triple9) -> rule5))]
("Gary" "is" "white" "-")
((triple9) -> (rule5 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is not cold.
False
2
inv-proof
[(((triple8) -> rule2) OR ((((triple12 triple9) -> rule1)) -> rule2))]
("Gary" "is" "cold" "-")
((triple8) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple12 triple9) -> (rule1 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "white" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "white" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Charlie is cold.[(triple1)] Charlie is nice.[(triple2)] Charlie is rough.[(triple3)] Dave is big.[(triple4)] Fiona is cold.[(triple5)] Fiona is not kind.[(triple6)] Fiona is quiet.[(triple7)] Gary is big.[(triple8 OR ((triple12 triple9) -> rule1))] Gary is kind.[(triple9)] Gary is nice.[(triple10)] Gary is not quiet.[(triple11)] Gary is rough.[(triple12)] @1: Dave is cold.[(((triple4) -> rule2))] Gary is cold.[(((triple8) -> rule2) OR ((((triple12 triple9) -> rule1)) -> rule2))] Gary is not white.[(((triple9) -> rule5))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Fiona is cold.
("Fiona" "is" "cold" "+")
triple5
Fiona is not kind.
("Fiona" "is" "kind" "-")
triple6
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple8
((triple12 triple9) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is nice.
("Gary" "is" "nice" "+")
triple10
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
Dave is cold.
("Dave" "is" "cold" "+")
((triple4) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple8) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple12 triple9) -> (rule1 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not white.
("Gary" "is" "white" "-")
((triple9) -> (rule5 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1