Anne is not cold. Anne is kind. Anne is young. Bob is nice. Charlie is cold. Gary is kind. Gary is nice. Nice, young things are quiet. All round, smart things are not quiet. If something is young and cold then it is kind. All cold things are young. Kind things are smart. If something is round and young then it is smart. If Bob is nice then Bob is not smart. All smart things are round. Quiet things are not round.
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Nice, young things are quiet.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
All round, smart things are not quiet.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "-"))
If something is young and cold then it is kind.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
All cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
Kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
If something is round and young then it is smart.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If Bob is nice then Bob is not smart.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "smart" "-"))
All smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Quiet things are not round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "-"))
Anne is not cold.
True
1
proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Gary is not kind.
False
1
inv-proof
[(triple6)]
("Gary" "is" "kind" "-")
triple6
Bob is not smart.
True
2
proof
[(((triple4) -> rule7))]
("Bob" "is" "smart" "-")
((triple4) -> (rule7 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Charlie is not young.
False
2
inv-proof
[(((triple5) -> rule4))]
("Charlie" "is" "young" "-")
((triple5) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Anne is round.
True
3
proof
[(((((triple2) -> rule5)) -> rule8))]
("Anne" "is" "round" "+")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Gary is not round.
False
3
inv-proof
[(((((triple6) -> rule5)) -> rule8))]
("Gary" "is" "round" "-")
((((triple6) -> (rule5 % int2))) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Charlie is smart.
True
5
proof
[(((((((triple5) -> rule4) triple5) -> rule3)) -> rule5))]
("Charlie" "is" "smart" "+")
((((((triple5) -> (rule4 % int3)) triple5) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Gary is quiet.
False
6
inv-proof
[(((((((triple6) -> rule5)) -> rule8) ((triple6) -> rule5)) -> rule2))]
("Gary" "is" "quiet" "+")
((((((triple6) -> (rule5 % int3))) -> (rule8 % int2)) ((triple6) -> (rule5 % int3))) -> (rule2 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Charlie is round.
True
6
proof
[(((((((((triple5) -> rule4) triple5) -> rule3)) -> rule5)) -> rule8))]
("Charlie" "is" "round" "+")
((((((((triple5) -> (rule4 % int4)) triple5) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is not round.
False
6
inv-proof
[(((((((((triple5) -> rule4) triple5) -> rule3)) -> rule5)) -> rule8))]
("Charlie" "is" "round" "-")
((((((((triple5) -> (rule4 % int4)) triple5) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is not quiet.
True
12
proof
[(((((((((((triple5) -> rule4) triple5) -> rule3)) -> rule5)) -> rule8) ((((((triple5) -> rule4) triple5) -> rule3)) -> rule5)) -> rule2))]
("Charlie" "is" "quiet" "-")
((((((((((triple5) -> (rule4 % int5)) triple5) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule8 % int2)) ((((((triple5) -> (rule4 % int5)) triple5) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule2 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is young.
("Charlie" "is" "young" "+")
int5
Charlie is quiet.
False
12
inv-proof
[(((((((((((triple5) -> rule4) triple5) -> rule3)) -> rule5)) -> rule8) ((((((triple5) -> rule4) triple5) -> rule3)) -> rule5)) -> rule2))]
("Charlie" "is" "quiet" "+")
((((((((((triple5) -> (rule4 % int5)) triple5) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule8 % int2)) ((((((triple5) -> (rule4 % int5)) triple5) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule2 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is young.
("Charlie" "is" "young" "+")
int5
Bob is not quiet.
Unknown
inv-rconc
[@2: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "young" "+")
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "young" "-")
Bob is kind.
Unknown
rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "kind" "+")
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "round" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Anne is kind.[(triple2)] Anne is not cold.[(triple1)] Anne is young.[(triple3)] Bob is nice.[(triple4)] Charlie is cold.[(triple5)] Gary is kind.[(triple6)] Gary is nice.[(triple7)] @1: Anne is smart.[(((triple2) -> rule5))] Bob is not smart.[(((triple4) -> rule7))] Charlie is young.[(((triple5) -> rule4))] Gary is smart.[(((triple6) -> rule5))] @2: Anne is round.[(((((triple2) -> rule5)) -> rule8))] Charlie is kind.[(((((triple5) -> rule4) triple5) -> rule3))] Gary is round.[(((((triple6) -> rule5)) -> rule8))] @3: Anne is not quiet.[(((((((triple2) -> rule5)) -> rule8) ((triple2) -> rule5)) -> rule2))] Charlie is smart.[(((((((triple5) -> rule4) triple5) -> rule3)) -> rule5))] Gary is not quiet.[(((((((triple6) -> rule5)) -> rule8) ((triple6) -> rule5)) -> rule2))] @4: Charlie is round.[(((((((((triple5) -> rule4) triple5) -> rule3)) -> rule5)) -> rule8))] @5: Charlie is not quiet.[(((((((((((triple5) -> rule4) triple5) -> rule3)) -> rule5)) -> rule8) ((((((triple5) -> rule4) triple5) -> rule3)) -> rule5)) -> rule2))]
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is not cold.
("Anne" "is" "cold" "-")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
Gary is kind.
("Gary" "is" "kind" "+")
triple6
Gary is nice.
("Gary" "is" "nice" "+")
triple7
Anne is smart.
("Anne" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is not smart.
("Bob" "is" "smart" "-")
((triple4) -> (rule7 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple5) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple6) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple5) -> (rule4 % int2)) triple5) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((triple6) -> (rule5 % int2))) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Anne is not quiet.
("Anne" "is" "quiet" "-")
((((((triple2) -> (rule5 % int3))) -> (rule8 % int2)) ((triple2) -> (rule5 % int3))) -> (rule2 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((triple5) -> (rule4 % int3)) triple5) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Gary is not quiet.
("Gary" "is" "quiet" "-")
((((((triple6) -> (rule5 % int3))) -> (rule8 % int2)) ((triple6) -> (rule5 % int3))) -> (rule2 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
((((((((triple5) -> (rule4 % int4)) triple5) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
((((((((((triple5) -> (rule4 % int5)) triple5) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule8 % int2)) ((((((triple5) -> (rule4 % int5)) triple5) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule2 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is young.
("Charlie" "is" "young" "+")
int5