Charlie is quiet. Charlie is red. Charlie is rough. Fiona is cold. Fiona is green. Fiona is red. Fiona is rough. Gary is cold. Gary is nice. Gary is quiet. Gary is red. Gary is rough. If someone is rough and green then they are cold. All nice people are green. All round people are cold. If someone is round and nice then they are quiet. If Charlie is red and Charlie is quiet then Charlie is nice. If someone is quiet then they are green. If someone is cold and round then they are rough. Round people are cold.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If someone is rough and green then they are cold.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
All nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
All round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If someone is round and nice then they are quiet.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If Charlie is red and Charlie is quiet then Charlie is nice.
((("Charlie" "is" "red" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "nice" "+"))
If someone is quiet then they are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If someone is cold and round then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Gary is red.
True
1
proof
[(triple11)]
("Gary" "is" "red" "+")
triple11
Gary is not quiet.
False
1
inv-proof
[(triple10)]
("Gary" "is" "quiet" "-")
triple10
Charlie is nice.
True
3
proof
[(((triple2 triple1) -> rule5))]
("Charlie" "is" "nice" "+")
((triple2 triple1) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
3
inv-proof
[(((triple2 triple1) -> rule5))]
("Charlie" "is" "nice" "-")
((triple2 triple1) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Charlie is quiet.[(triple1)] Charlie is red.[(triple2)] Charlie is rough.[(triple3)] Fiona is cold.[(triple4 OR ((triple7 triple5) -> rule1))] Fiona is green.[(triple5)] Fiona is red.[(triple6)] Fiona is rough.[(triple7)] Gary is cold.[(triple8 OR ((triple12 ((triple10) -> rule6)) -> rule1) OR ((triple12 ((triple9) -> rule2)) -> rule1))] Gary is nice.[(triple9)] Gary is quiet.[(triple10)] Gary is red.[(triple11)] Gary is rough.[(triple12)] @1: Charlie is green.[(((triple1) -> rule6) OR ((((triple2 triple1) -> rule5)) -> rule2))] Charlie is nice.[(((triple2 triple1) -> rule5))] Gary is green.[(((triple10) -> rule6) OR ((triple9) -> rule2))] @2: Charlie is cold.[(((triple3 ((triple1) -> rule6)) -> rule1) OR ((triple3 ((((triple2 triple1) -> rule5)) -> rule2)) -> rule1))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple4
((triple7 triple5) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
triple5
Fiona is red.
("Fiona" "is" "red" "+")
triple6
Fiona is rough.
("Fiona" "is" "rough" "+")
triple7
Gary is cold.
("Gary" "is" "cold" "+")
triple8
((triple12 ((triple10) -> (rule6 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((triple12 ((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple2 triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2 triple1) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple10) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple9) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3 ((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((triple3 ((((triple2 triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3