Anne is white. Charlie is smart. Fiona is not round. Gary is cold. White things are big. Young, round things are big. All young things are cold. All smart, big things are cold. If Anne is not round then Anne is not cold. All smart things are white.
Anne is white.
("Anne" "is" "white" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
Gary is cold.
("Gary" "is" "cold" "+")
White things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Young, round things are big.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
All smart, big things are cold.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If Anne is not round then Anne is not cold.
((("Anne" "is" "round" "~")) -> ("Anne" "is" "cold" "-"))
All smart things are white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
Anne is white.
True
1
proof
[(triple1)]
("Anne" "is" "white" "+")
triple1
Anne is not white.
False
1
inv-proof
[(triple1)]
("Anne" "is" "white" "-")
triple1
Charlie is white.
True
2
proof
[(((triple2) -> rule6))]
("Charlie" "is" "white" "+")
((triple2) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple2) -> rule6))]
("Charlie" "is" "white" "-")
((triple2) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
True
3
proof
[(((((triple2) -> rule6)) -> rule1))]
("Charlie" "is" "big" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not big.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule1))]
("Charlie" "is" "big" "-")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is cold.
True
5
proof
[(((triple2 ((((triple2) -> rule6)) -> rule1)) -> rule4))]
("Charlie" "is" "cold" "+")
((triple2 ((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not cold.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule6)) -> rule1)) -> rule4))]
("Charlie" "is" "cold" "-")
((triple2 ((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Fiona is not big.
Unknown
inv-rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Fiona" "is" "big" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "white" "+")
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "white" "-")
Fiona is cold.
Unknown
rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "cold" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Anne is white.[(triple1)] Charlie is smart.[(triple2)] Fiona is not round.[(triple3)] Gary is cold.[(triple4)] @1: Anne is big.[(((triple1) -> rule1))] Charlie is white.[(((triple2) -> rule6))] @2: Charlie is big.[(((((triple2) -> rule6)) -> rule1))] @3: Charlie is cold.[(((triple2 ((((triple2) -> rule6)) -> rule1)) -> rule4))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Fiona is not round.
("Fiona" "is" "round" "-")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple2) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple2 ((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3