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