Anne is young. Bob is nice. Bob is not smart. Charlie is young. Fiona is kind. Fiona is nice. Fiona is not young. All young, kind people are smart. Young, nice people are kind. All young people are nice. If Fiona is kind then Fiona is red. If someone is round and not kind then they are red. If someone is red and not kind then they are round. If Charlie is cold then Charlie is red. If Anne is round and Anne is not nice then Anne is smart. Smart, nice people are cold.
Anne is young.
("Anne" "is" "young" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is not young.
("Fiona" "is" "young" "-")
All young, kind people are smart.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
Young, nice people are kind.
((("someone" "is" "young" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All young people are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If Fiona is kind then Fiona is red.
((("Fiona" "is" "kind" "+")) -> ("Fiona" "is" "red" "+"))
If someone is round and not kind then they are red.
((("someone" "is" "round" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "red" "+"))
If someone is red and not kind then they are round.
((("someone" "is" "red" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "round" "+"))
If Charlie is cold then Charlie is red.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "red" "+"))
If Anne is round and Anne is not nice then Anne is smart.
((("Anne" "is" "round" "+") ("Anne" "is" "nice" "~")) -> ("Anne" "is" "smart" "+"))
Smart, nice people are cold.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Bob is nice.
True
1
proof
[(triple2)]
("Bob" "is" "nice" "+")
triple2
Fiona is not kind.
False
1
inv-proof
[(triple5)]
("Fiona" "is" "kind" "-")
triple5
Charlie is nice.
True
2
proof
[(((triple4) -> rule3))]
("Charlie" "is" "nice" "+")
((triple4) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Fiona is not red.
False
2
inv-proof
[(((triple5) -> rule4))]
("Fiona" "is" "red" "-")
((triple5) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Anne is kind.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule2))]
("Anne" "is" "kind" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not kind.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule2))]
("Anne" "is" "kind" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Charlie is smart.
True
6
proof
[(((triple4 ((triple4 ((triple4) -> rule3)) -> rule2)) -> rule1))]
("Charlie" "is" "smart" "+")
((triple4 ((triple4 ((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Anne is not smart.
False
6
inv-proof
[(((triple1 ((triple1 ((triple1) -> rule3)) -> rule2)) -> rule1))]
("Anne" "is" "smart" "-")
((triple1 ((triple1 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is cold.
True
9
proof
[(((((triple1 ((triple1 ((triple1) -> rule3)) -> rule2)) -> rule1) ((triple1) -> rule3)) -> rule9))]
("Anne" "is" "cold" "+")
((((triple1 ((triple1 ((triple1) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule3 % int4))) -> (rule9 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is not cold.
False
9
inv-proof
[(((((triple1 ((triple1 ((triple1) -> rule3)) -> rule2)) -> rule1) ((triple1) -> rule3)) -> rule9))]
("Anne" "is" "cold" "-")
((((triple1 ((triple1 ((triple1) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule3 % int4))) -> (rule9 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Charlie is red.
True
10
proof
[(((((((triple4 ((triple4 ((triple4) -> rule3)) -> rule2)) -> rule1) ((triple4) -> rule3)) -> rule9)) -> rule7))]
("Charlie" "is" "red" "+")
((((((triple4 ((triple4 ((triple4) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule1 % int3)) ((triple4) -> (rule3 % int5))) -> (rule9 % int2))) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
int5
Charlie is not red.
False
10
inv-proof
[(((((((triple4 ((triple4 ((triple4) -> rule3)) -> rule2)) -> rule1) ((triple4) -> rule3)) -> rule9)) -> rule7))]
("Charlie" "is" "red" "-")
((((((triple4 ((triple4 ((triple4) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule1 % int3)) ((triple4) -> (rule3 % int5))) -> (rule9 % int2))) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
int5
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "round" "-")
Bob is kind.
Unknown
rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "kind" "+")
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "red" "-")
Fiona is smart.
Unknown
rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not cold.
Unknown
inv-rconc
[@2: Fiona is cold.[CWA. Example of deepest failure = (rule9 <- rule1 <- FAIL)]]
("Fiona" "is" "cold" "-")
Bob is round.
Unknown
rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "round" "+")
@0: Anne is young.[(triple1)] Bob is nice.[(triple2)] Bob is not smart.[(triple3)] Charlie is young.[(triple4)] Fiona is kind.[(triple5)] Fiona is nice.[(triple6)] Fiona is not young.[(triple7)] @1: Anne is nice.[(((triple1) -> rule3))] Charlie is nice.[(((triple4) -> rule3))] Fiona is red.[(((triple5) -> rule4))] @2: Anne is kind.[(((triple1 ((triple1) -> rule3)) -> rule2))] Charlie is kind.[(((triple4 ((triple4) -> rule3)) -> rule2))] @3: Anne is smart.[(((triple1 ((triple1 ((triple1) -> rule3)) -> rule2)) -> rule1))] Charlie is smart.[(((triple4 ((triple4 ((triple4) -> rule3)) -> rule2)) -> rule1))] @4: Anne is cold.[(((((triple1 ((triple1 ((triple1) -> rule3)) -> rule2)) -> rule1) ((triple1) -> rule3)) -> rule9))] Charlie is cold.[(((((triple4 ((triple4 ((triple4) -> rule3)) -> rule2)) -> rule1) ((triple4) -> rule3)) -> rule9))] @5: Charlie is red.[(((((((triple4 ((triple4 ((triple4) -> rule3)) -> rule2)) -> rule1) ((triple4) -> rule3)) -> rule9)) -> rule7))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is not smart.
("Bob" "is" "smart" "-")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Fiona is kind.
("Fiona" "is" "kind" "+")
triple5
Fiona is nice.
("Fiona" "is" "nice" "+")
triple6
Fiona is not young.
("Fiona" "is" "young" "-")
triple7
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple4) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple5) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple4 ((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((triple1 ((triple1 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple4 ((triple4 ((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1 ((triple1 ((triple1) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule3 % int4))) -> (rule9 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple4 ((triple4 ((triple4) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) ((triple4) -> (rule3 % int4))) -> (rule9 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is red.
("Charlie" "is" "red" "+")
((((((triple4 ((triple4 ((triple4) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule1 % int3)) ((triple4) -> (rule3 % int5))) -> (rule9 % int2))) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
int5