Anne is young. Bob is cold. Charlie is not nice. Gary is quiet. If something is rough then it is cold. If something is green then it is cold. If something is quiet then it is cold. If Anne is young and Anne is cold then Anne is not nice. Young things are rough. If something is nice and quiet then it is rough. If something is green and not young then it is nice. Cold, young things are round.
Anne is young.
("Anne" "is" "young" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Gary is quiet.
("Gary" "is" "quiet" "+")
If something is rough then it is cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something is green then it is cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something is quiet then it is cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If Anne is young and Anne is cold then Anne is not nice.
((("Anne" "is" "young" "+") ("Anne" "is" "cold" "+")) -> ("Anne" "is" "nice" "-"))
Young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If something is nice and quiet then it is rough.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is green and not young then it is nice.
((("something" "is" "green" "+") ("something" "is" "young" "~")) -> ("something" "is" "nice" "+"))
Cold, young things are round.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
Gary is quiet.
True
1
proof
[(triple4)]
("Gary" "is" "quiet" "+")
triple4
Charlie is nice.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "nice" "+")
triple3
Anne is rough.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "rough" "+")
((triple1) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not rough.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "rough" "-")
((triple1) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is cold.
True
3
proof
[(((((triple1) -> rule5)) -> rule1))]
("Anne" "is" "cold" "+")
((((triple1) -> (rule5 % 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
[(((((triple1) -> rule5)) -> rule1))]
("Anne" "is" "cold" "-")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not nice.
True
5
proof
[(((triple1 ((((triple1) -> rule5)) -> rule1)) -> rule4))]
("Anne" "is" "nice" "-")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not round.
False
5
inv-proof
[(((((((triple1) -> rule5)) -> rule1) triple1) -> rule8))]
("Anne" "is" "round" "-")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2)) triple1) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "nice" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "round" "-")
Gary is rough.
Unknown
rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Gary" "is" "rough" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Anne is young.[(triple1)] Bob is cold.[(triple2)] Charlie is not nice.[(triple3)] Gary is quiet.[(triple4)] @1: Anne is rough.[(((triple1) -> rule5))] Gary is cold.[(((triple4) -> rule3))] @2: Anne is cold.[(((((triple1) -> rule5)) -> rule1))] @3: Anne is not nice.[(((triple1 ((((triple1) -> rule5)) -> rule1)) -> rule4))] Anne is round.[(((((((triple1) -> rule5)) -> rule1) triple1) -> rule8))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple4) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not nice.
("Anne" "is" "nice" "-")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2)) triple1) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3