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