Anne is big. Anne is blue. Charlie is rough. Fiona is blue. Gary is cold. Gary is nice. Gary is not rough. If something is rough then it is cold. If Anne is rough and Anne is not nice then Anne is quiet. Cold things are quiet. If Gary is blue and Gary is not nice then Gary is not rough. Big, quiet things are round. If Anne is blue then Anne is rough.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
If something is rough then it is cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If Anne is rough and Anne is not nice then Anne is quiet.
((("Anne" "is" "rough" "+") ("Anne" "is" "nice" "~")) -> ("Anne" "is" "quiet" "+"))
Cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
If Gary is blue and Gary is not nice then Gary is not rough.
((("Gary" "is" "blue" "+") ("Gary" "is" "nice" "~")) -> ("Gary" "is" "rough" "-"))
Big, quiet things are round.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If Anne is blue then Anne is rough.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "rough" "+"))
Charlie is rough.
True
1
proof
[(triple3)]
("Charlie" "is" "rough" "+")
triple3
Gary is not cold.
False
1
inv-proof
[(triple5)]
("Gary" "is" "cold" "-")
triple5
Charlie is cold.
True
2
proof
[(((triple3) -> rule1))]
("Charlie" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple3) -> rule1))]
("Charlie" "is" "cold" "-")
((triple3) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Anne is cold.
True
3
proof
[(((((triple2) -> rule6)) -> rule1))]
("Anne" "is" "cold" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not cold.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule1))]
("Anne" "is" "cold" "-")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
True
4
proof
[(((((((triple2) -> rule6)) -> rule1)) -> rule3))]
("Anne" "is" "quiet" "+")
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not quiet.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule1)) -> rule3))]
("Anne" "is" "quiet" "-")
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "round" "-")
Fiona is cold.
Unknown
rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "cold" "+")
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "round" "-")
Fiona is round.
Unknown
rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "round" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Charlie is rough.[(triple3)] Fiona is blue.[(triple4)] Gary is cold.[(triple5)] Gary is nice.[(triple6)] Gary is not rough.[(triple7)] @1: Anne is rough.[(((triple2) -> rule6))] Charlie is cold.[(((triple3) -> rule1))] Gary is quiet.[(((triple5) -> rule3))] @2: Anne is cold.[(((((triple2) -> rule6)) -> rule1))] Charlie is quiet.[(((((triple3) -> rule1)) -> rule3))] @3: Anne is quiet.[(((((((triple2) -> rule6)) -> rule1)) -> rule3))] @4: Anne is round.[(((triple1 ((((((triple2) -> rule6)) -> rule1)) -> rule3)) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Fiona is blue.
("Fiona" "is" "blue" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Gary is not rough.
("Gary" "is" "rough" "-")
triple7
Anne is rough.
("Anne" "is" "rough" "+")
((triple2) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple5) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
((triple1 ((((((triple2) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4