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