Charlie is cold. Erin is big. Fiona is red. Gary is cold. Cold, quiet things are green. If something is big and green then it is quiet. If something is big and cold then it is green. Red things are big. Cold things are red. If something is quiet then it is big.
Charlie is cold.
("Charlie" "is" "cold" "+")
Erin is big.
("Erin" "is" "big" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Cold, quiet things are green.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If something is big and green then it is quiet.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is big and cold then it is green.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
Red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If something is quiet then it is big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
Erin is big.
True
1
proof
[(triple2)]
("Erin" "is" "big" "+")
triple2
Gary is not cold.
False
1
inv-proof
[(triple4)]
("Gary" "is" "cold" "-")
triple4
Charlie is red.
True
2
proof
[(((triple1) -> rule5))]
("Charlie" "is" "red" "+")
((triple1) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Gary is not red.
False
2
inv-proof
[(((triple4) -> rule5))]
("Gary" "is" "red" "-")
((triple4) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Charlie is big.
True
3
proof
[(((((triple1) -> rule5)) -> rule4))]
("Charlie" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Gary is not big.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule4))]
("Gary" "is" "big" "-")
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is green.
True
5
proof
[(((((((triple4) -> rule5)) -> rule4) triple4) -> rule3))]
("Gary" "is" "green" "+")
((((((triple4) -> (rule5 % int3))) -> (rule4 % int2)) triple4) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is not green.
False
5
inv-proof
[(((((((triple4) -> rule5)) -> rule4) triple4) -> rule3))]
("Gary" "is" "green" "-")
((((((triple4) -> (rule5 % int3))) -> (rule4 % int2)) triple4) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "green" "-")
Erin is green.
Unknown
rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "green" "+")
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "red" "-")
Fiona is quiet.
Unknown
rconc
[@2: Fiona is quiet.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Charlie is cold.[(triple1)] Erin is big.[(triple2)] Fiona is red.[(triple3)] Gary is cold.[(triple4)] @1: Charlie is red.[(((triple1) -> rule5))] Fiona is big.[(((triple3) -> rule4))] Gary is red.[(((triple4) -> rule5))] @2: Charlie is big.[(((((triple1) -> rule5)) -> rule4))] Gary is big.[(((((triple4) -> rule5)) -> rule4))] @3: Charlie is green.[(((((((triple1) -> rule5)) -> rule4) triple1) -> rule3))] Gary is green.[(((((((triple4) -> rule5)) -> rule4) triple4) -> rule3))] @4: Charlie is quiet.[(((((((triple1) -> rule5)) -> rule4) ((((((triple1) -> rule5)) -> rule4) triple1) -> rule3)) -> rule2))] Gary is quiet.[(((((((triple4) -> rule5)) -> rule4) ((((((triple4) -> rule5)) -> rule4) triple4) -> rule3)) -> rule2))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
Fiona is red.
("Fiona" "is" "red" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
((triple1) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple3) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple4) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((((((triple4) -> (rule5 % int3))) -> (rule4 % int2)) triple4) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((((triple1) -> (rule5 % int4))) -> (rule4 % int3)) ((((((triple1) -> (rule5 % int4))) -> (rule4 % int3)) triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((triple4) -> (rule5 % int4))) -> (rule4 % int3)) ((((((triple4) -> (rule5 % int4))) -> (rule4 % int3)) triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4