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