Anne is smart. Bob is blue. Bob is kind. Charlie is smart. Charlie is young. Fiona is green. Fiona is kind. If something is red then it is round. Red, blue things are green. Smart things are round. If something is round then it is red. If Bob is round then Bob is kind. If Anne is green then Anne is smart. All red things are kind. If Anne is round and Anne is kind then Anne is blue.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
If something is red then it is round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
Red, blue things are green.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
If something is round then it is red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If Bob is round then Bob is kind.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "kind" "+"))
If Anne is green then Anne is smart.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "smart" "+"))
All red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If Anne is round and Anne is kind then Anne is blue.
((("Anne" "is" "round" "+") ("Anne" "is" "kind" "+")) -> ("Anne" "is" "blue" "+"))
Bob is kind.
True
1
proof
[(triple3)]
("Bob" "is" "kind" "+")
triple3
Fiona is not kind.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "kind" "-")
triple7
Anne is round.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "round" "+")
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple4) -> rule3))]
("Charlie" "is" "round" "-")
((triple4) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
True
3
proof
[(((((triple4) -> rule3)) -> rule4))]
("Charlie" "is" "red" "+")
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Anne is not red.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule4))]
("Anne" "is" "red" "-")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Charlie is kind.
True
4
proof
[(((((((triple4) -> rule3)) -> rule4)) -> rule7))]
("Charlie" "is" "kind" "+")
((((((triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Anne is not kind.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule4)) -> rule7))]
("Anne" "is" "kind" "-")
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is blue.
True
7
proof
[(((((triple1) -> rule3) ((((((triple1) -> rule3)) -> rule4)) -> rule7)) -> rule8))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule3 % int4)) ((((((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is not blue.
False
7
inv-proof
[(((((triple1) -> rule3) ((((((triple1) -> rule3)) -> rule4)) -> rule7)) -> rule8))]
("Anne" "is" "blue" "-")
((((triple1) -> (rule3 % int4)) ((((((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is green.
True
11
proof
[(((((((triple1) -> rule3)) -> rule4) ((((triple1) -> rule3) ((((((triple1) -> rule3)) -> rule4)) -> rule7)) -> rule8)) -> rule2))]
("Anne" "is" "green" "+")
((((((triple1) -> (rule3 % int5))) -> (rule4 % int4)) ((((triple1) -> (rule3 % int5)) ((((((triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
Anne is not green.
False
11
inv-proof
[(((((((triple1) -> rule3)) -> rule4) ((((triple1) -> rule3) ((((((triple1) -> rule3)) -> rule4)) -> rule7)) -> rule8)) -> rule2))]
("Anne" "is" "green" "-")
((((((triple1) -> (rule3 % int5))) -> (rule4 % int4)) ((((triple1) -> (rule3 % int5)) ((((((triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
Fiona is not red.
Unknown
inv-rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Fiona" "is" "red" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "+")
Bob is not green.
Unknown
inv-rconc
[@3: Bob is green.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule1 <- FAIL)]]
("Bob" "is" "green" "-")
Fiona is round.
Unknown
rconc
[@3: Fiona is round.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule3 <- FAIL)]]
("Fiona" "is" "round" "+")
Bob is not red.
Unknown
inv-rconc
[@2: Bob is red.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Bob" "is" "red" "-")
Bob is round.
Unknown
rconc
[@3: Bob is round.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule3 <- FAIL)]]
("Bob" "is" "round" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Anne is smart.[(triple1)] Bob is blue.[(triple2)] Bob is kind.[(triple3)] Charlie is smart.[(triple4)] Charlie is young.[(triple5)] Fiona is green.[(triple6)] Fiona is kind.[(triple7)] @1: Anne is round.[(((triple1) -> rule3))] Charlie is round.[(((triple4) -> rule3))] @2: Anne is red.[(((((triple1) -> rule3)) -> rule4))] Charlie is red.[(((((triple4) -> rule3)) -> rule4))] @3: Anne is kind.[(((((((triple1) -> rule3)) -> rule4)) -> rule7))] Charlie is kind.[(((((((triple4) -> rule3)) -> rule4)) -> rule7))] @4: Anne is blue.[(((((triple1) -> rule3) ((((((triple1) -> rule3)) -> rule4)) -> rule7)) -> rule8))] @5: Anne is green.[(((((((triple1) -> rule3)) -> rule4) ((((triple1) -> rule3) ((((((triple1) -> rule3)) -> rule4)) -> rule7)) -> rule8)) -> rule2))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Fiona is green.
("Fiona" "is" "green" "+")
triple6
Fiona is kind.
("Fiona" "is" "kind" "+")
triple7
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple4) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
((((((triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule3 % int4)) ((((((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
((((((triple1) -> (rule3 % int5))) -> (rule4 % int4)) ((((triple1) -> (rule3 % int5)) ((((((triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5