Bob is nice. Bob is white. Charlie is green. Charlie is white. Erin is big. Erin is young. Harry is big. Harry is kind. Harry is nice. Harry is red. Harry is white. Harry is young. Red, big things are nice. If Erin is nice then Erin is big. Big, red things are young. Big, red things are white. Nice, big things are red. Nice things are big. Green things are nice. All big, nice things are white.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
Red, big things are nice.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If Erin is nice then Erin is big.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "big" "+"))
Big, red things are young.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Big, red things are white.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
Nice, big things are red.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
Nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
All big, nice things are white.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Harry is red.
True
1
proof
[(triple10 OR ((triple9 triple7) -> rule5) OR ((triple9 ((triple9) -> rule6)) -> rule5))]
("Harry" "is" "red" "+")
triple10
((triple9 triple7) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple9 ((triple9) -> (rule6 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Bob is not white.
False
1
inv-proof
[(triple2 OR ((((triple1) -> rule6) triple1) -> rule8) OR ((((triple1) -> rule6) ((triple1 ((triple1) -> rule6)) -> rule5)) -> rule4))]
("Bob" "is" "white" "-")
triple2
((((triple1) -> (rule6 % int2)) triple1) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple1) -> (rule6 % int3)) ((triple1 ((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is big.
True
2
proof
[(((triple1) -> rule6))]
("Bob" "is" "big" "+")
((triple1) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple3) -> rule7))]
("Charlie" "is" "nice" "-")
((triple3) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
True
3
proof
[(((((triple3) -> rule7)) -> rule6))]
("Charlie" "is" "big" "+")
((((triple3) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Bob is not red.
False
4
inv-proof
[(((triple1 ((triple1) -> rule6)) -> rule5))]
("Bob" "is" "red" "-")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
True
7
proof
[(((((triple1) -> rule6) ((triple1 ((triple1) -> rule6)) -> rule5)) -> rule3))]
("Bob" "is" "young" "+")
((((triple1) -> (rule6 % int3)) ((triple1 ((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is not young.
False
7
inv-proof
[(((((triple1) -> rule6) ((triple1 ((triple1) -> rule6)) -> rule5)) -> rule3))]
("Bob" "is" "young" "-")
((((triple1) -> (rule6 % int3)) ((triple1 ((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Erin is not nice.
Unknown
inv-rconc
[@3: Erin is nice.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule7 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is white.
Unknown
rconc
[@4: Erin is white.[CWA. Example of deepest failure = (rule8 <- rule1 <- rule5 <- rule7 <- FAIL)]]
("Erin" "is" "white" "+")
Erin is not red.
Unknown
inv-rconc
[@2: Erin is red.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Erin" "is" "red" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Bob is nice.[(triple1)] Bob is white.[(triple2 OR ((((triple1) -> rule6) triple1) -> rule8) OR ((((triple1) -> rule6) ((triple1 ((triple1) -> rule6)) -> rule5)) -> rule4))] Charlie is green.[(triple3)] Charlie is white.[(triple4 OR ((((((triple3) -> rule7)) -> rule6) ((triple3) -> rule7)) -> rule8) OR ((((((triple3) -> rule7)) -> rule6) ((((triple3) -> rule7) ((((triple3) -> rule7)) -> rule6)) -> rule5)) -> rule4))] Erin is big.[(triple5)] Erin is young.[(triple6)] Harry is big.[(triple7 OR ((triple9) -> rule6))] Harry is kind.[(triple8)] Harry is nice.[(triple9 OR ((triple10 triple7) -> rule1))] Harry is red.[(triple10 OR ((triple9 triple7) -> rule5) OR ((triple9 ((triple9) -> rule6)) -> rule5))] Harry is white.[(triple11 OR ((triple7 triple10) -> rule4) OR ((triple7 triple9) -> rule8) OR ((triple7 ((triple10 triple7) -> rule1)) -> rule8) OR ((triple7 ((triple9 triple7) -> rule5)) -> rule4) OR ((((triple9) -> rule6) triple10) -> rule4) OR ((((triple9) -> rule6) triple9) -> rule8) OR ((((triple9) -> rule6) ((triple10 triple7) -> rule1)) -> rule8) OR ((((triple9) -> rule6) ((triple9 triple7) -> rule5)) -> rule4) OR ((triple7 ((triple9 ((triple9) -> rule6)) -> rule5)) -> rule4) OR ((((triple9) -> rule6) ((triple9 ((triple9) -> rule6)) -> rule5)) -> rule4))] Harry is young.[(triple12 OR ((triple7 triple10) -> rule3) OR ((triple7 ((triple9 triple7) -> rule5)) -> rule3) OR ((((triple9) -> rule6) triple10) -> rule3) OR ((((triple9) -> rule6) ((triple9 triple7) -> rule5)) -> rule3) OR ((triple7 ((triple9 ((triple9) -> rule6)) -> rule5)) -> rule3) OR ((((triple9) -> rule6) ((triple9 ((triple9) -> rule6)) -> rule5)) -> rule3))] @1: Bob is big.[(((triple1) -> rule6))] Charlie is nice.[(((triple3) -> rule7))] @2: Bob is red.[(((triple1 ((triple1) -> rule6)) -> rule5))] Charlie is big.[(((((triple3) -> rule7)) -> rule6))] @3: Bob is young.[(((((triple1) -> rule6) ((triple1 ((triple1) -> rule6)) -> rule5)) -> rule3))] Charlie is red.[(((((triple3) -> rule7) ((((triple3) -> rule7)) -> rule6)) -> rule5))] @4: Charlie is young.[(((((((triple3) -> rule7)) -> rule6) ((((triple3) -> rule7) ((((triple3) -> rule7)) -> rule6)) -> rule5)) -> rule3))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
((((triple1) -> (rule6 % int2)) triple1) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple1) -> (rule6 % int3)) ((triple1 ((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
((((((triple3) -> (rule7 % int3))) -> (rule6 % int2)) ((triple3) -> (rule7 % int3))) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((((((triple3) -> (rule7 % int4))) -> (rule6 % int3)) ((((triple3) -> (rule7 % int4)) ((((triple3) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is young.
("Erin" "is" "young" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
((triple9) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
((triple10 triple7) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple10
((triple9 triple7) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple9 ((triple9) -> (rule6 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
triple11
((triple7 triple10) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple7 triple9) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple7 ((triple10 triple7) -> (rule1 % int2))) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple7 ((triple9 triple7) -> (rule5 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple9) -> (rule6 % int2)) triple10) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple9) -> (rule6 % int2)) triple9) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple9) -> (rule6 % int3)) ((triple10 triple7) -> (rule1 % int2))) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((triple9) -> (rule6 % int3)) ((triple9 triple7) -> (rule5 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((triple7 ((triple9 ((triple9) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((triple9) -> (rule6 % int3)) ((triple9 ((triple9) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
triple12
((triple7 triple10) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple7 ((triple9 triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple9) -> (rule6 % int2)) triple10) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple9) -> (rule6 % int3)) ((triple9 triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((triple7 ((triple9 ((triple9) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((triple9) -> (rule6 % int3)) ((triple9 ((triple9) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple3) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((((triple3) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((triple1) -> (rule6 % int3)) ((triple1 ((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
((((triple3) -> (rule7 % int3)) ((((triple3) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
((((((triple3) -> (rule7 % int4))) -> (rule6 % int3)) ((((triple3) -> (rule7 % int4)) ((((triple3) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4