Bob is big. Bob is green. Dave is big. Erin is nice. Fiona is big. Fiona is nice. Fiona is young. Blue things are white. All nice things are green. All big, smart things are young. Nice, green things are smart. If something is nice and young then it is blue. All nice things are big. All blue, green things are young. All blue things are young.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Dave is big.
("Dave" "is" "big" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
All nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
All big, smart things are young.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Nice, green things are smart.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If something is nice and young then it is blue.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
All nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
All blue, green things are young.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
All blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Dave is big.
True
1
proof
[(triple3)]
("Dave" "is" "big" "+")
triple3
Fiona is not young.
False
1
inv-proof
[(triple7 OR ((triple5 ((triple6 ((triple6) -> rule2)) -> rule4)) -> rule3) OR ((((triple6) -> rule6) ((triple6 ((triple6) -> rule2)) -> rule4)) -> rule3))]
("Fiona" "is" "young" "-")
triple7
((triple5 ((triple6 ((triple6) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
((((triple6) -> (rule6 % int4)) ((triple6 ((triple6) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Fiona is blue.
True
3
proof
[(((triple6 triple7) -> rule5) OR ((triple6 ((triple5 ((triple6 ((triple6) -> rule2)) -> rule4)) -> rule3)) -> rule5) OR ((triple6 ((((triple6) -> rule6) ((triple6 ((triple6) -> rule2)) -> rule4)) -> rule3)) -> rule5))]
("Fiona" "is" "blue" "+")
((triple6 triple7) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple6 ((triple5 ((triple6 ((triple6) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % 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" "+")
int4
((triple6 ((((triple6) -> (rule6 % int5)) ((triple6 ((triple6) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % 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" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
int5
Fiona is not blue.
False
3
inv-proof
[(((triple6 triple7) -> rule5) OR ((triple6 ((triple5 ((triple6 ((triple6) -> rule2)) -> rule4)) -> rule3)) -> rule5) OR ((triple6 ((((triple6) -> rule6) ((triple6 ((triple6) -> rule2)) -> rule4)) -> rule3)) -> rule5))]
("Fiona" "is" "blue" "-")
((triple6 triple7) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple6 ((triple5 ((triple6 ((triple6) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % 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" "+")
int4
((triple6 ((((triple6) -> (rule6 % int5)) ((triple6 ((triple6) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % 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" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
int5
Fiona is smart.
True
4
proof
[(((triple6 ((triple6) -> rule2)) -> rule4))]
("Fiona" "is" "smart" "+")
((triple6 ((triple6) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is not white.
False
4
inv-proof
[(((((triple6 triple7) -> rule5)) -> rule1) OR ((((triple6 ((triple5 ((triple6 ((triple6) -> rule2)) -> rule4)) -> rule3)) -> rule5)) -> rule1) OR ((((triple6 ((((triple6) -> rule6) ((triple6 ((triple6) -> rule2)) -> rule4)) -> rule3)) -> rule5)) -> rule1))]
("Fiona" "is" "white" "-")
((((triple6 triple7) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((((triple6 ((triple5 ((triple6 ((triple6) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is green.
("Fiona" "is" "green" "+")
int5
((((triple6 ((((triple6) -> (rule6 % int6)) ((triple6 ((triple6) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is green.
("Fiona" "is" "green" "+")
int5
Fiona is big.
("Fiona" "is" "big" "+")
int6
Erin is young.
True
7
proof
[(((((triple4) -> rule6) ((triple4 ((triple4) -> rule2)) -> rule4)) -> rule3))]
("Erin" "is" "young" "+")
((((triple4) -> (rule6 % int4)) ((triple4 ((triple4) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is not young.
False
7
inv-proof
[(((((triple4) -> rule6) ((triple4 ((triple4) -> rule2)) -> rule4)) -> rule3))]
("Erin" "is" "young" "-")
((((triple4) -> (rule6 % int4)) ((triple4 ((triple4) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is blue.
True
9
proof
[(((triple4 ((((triple4) -> rule6) ((triple4 ((triple4) -> rule2)) -> rule4)) -> rule3)) -> rule5))]
("Erin" "is" "blue" "+")
((triple4 ((((triple4) -> (rule6 % int5)) ((triple4 ((triple4) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
int5
Erin is not blue.
False
9
inv-proof
[(((triple4 ((((triple4) -> rule6) ((triple4 ((triple4) -> rule2)) -> rule4)) -> rule3)) -> rule5))]
("Erin" "is" "blue" "-")
((triple4 ((((triple4) -> (rule6 % int5)) ((triple4 ((triple4) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
int5
Erin is white.
True
10
proof
[(((((triple4 ((((triple4) -> rule6) ((triple4 ((triple4) -> rule2)) -> rule4)) -> rule3)) -> rule5)) -> rule1))]
("Erin" "is" "white" "+")
((((triple4 ((((triple4) -> (rule6 % int6)) ((triple4 ((triple4) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
int5
Erin is big.
("Erin" "is" "big" "+")
int6
Erin is not white.
False
10
inv-proof
[(((((triple4 ((((triple4) -> rule6) ((triple4 ((triple4) -> rule2)) -> rule4)) -> rule3)) -> rule5)) -> rule1))]
("Erin" "is" "white" "-")
((((triple4 ((((triple4) -> (rule6 % int6)) ((triple4 ((triple4) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
int5
Erin is big.
("Erin" "is" "big" "+")
int6
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "blue" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "smart" "+")
Dave is not white.
Unknown
inv-rconc
[@2: Dave is white.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Dave" "is" "white" "-")
Bob is white.
Unknown
rconc
[@2: Bob is white.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Bob" "is" "white" "+")
Dave is not young.
Unknown
inv-rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Dave" "is" "young" "-")
Dave is blue.
Unknown
rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "blue" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Bob is big.[(triple1)] Bob is green.[(triple2)] Dave is big.[(triple3)] Erin is nice.[(triple4)] Fiona is big.[(triple5 OR ((triple6) -> rule6))] Fiona is nice.[(triple6)] Fiona is young.[(triple7 OR ((triple5 ((triple6 ((triple6) -> rule2)) -> rule4)) -> rule3) OR ((((triple6) -> rule6) ((triple6 ((triple6) -> rule2)) -> rule4)) -> rule3))] @1: Erin is big.[(((triple4) -> rule6))] Erin is green.[(((triple4) -> rule2))] Fiona is blue.[(((triple6 triple7) -> rule5) OR ((triple6 ((triple5 ((triple6 ((triple6) -> rule2)) -> rule4)) -> rule3)) -> rule5) OR ((triple6 ((((triple6) -> rule6) ((triple6 ((triple6) -> rule2)) -> rule4)) -> rule3)) -> rule5))] Fiona is green.[(((triple6) -> rule2))] @2: Erin is smart.[(((triple4 ((triple4) -> rule2)) -> rule4))] Fiona is smart.[(((triple6 ((triple6) -> rule2)) -> rule4))] Fiona is white.[(((((triple6 triple7) -> rule5)) -> rule1) OR ((((triple6 ((triple5 ((triple6 ((triple6) -> rule2)) -> rule4)) -> rule3)) -> rule5)) -> rule1) OR ((((triple6 ((((triple6) -> rule6) ((triple6 ((triple6) -> rule2)) -> rule4)) -> rule3)) -> rule5)) -> rule1))] @3: Erin is young.[(((((triple4) -> rule6) ((triple4 ((triple4) -> rule2)) -> rule4)) -> rule3))] @4: Erin is blue.[(((triple4 ((((triple4) -> rule6) ((triple4 ((triple4) -> rule2)) -> rule4)) -> rule3)) -> rule5))] @5: Erin is white.[(((((triple4 ((((triple4) -> rule6) ((triple4 ((triple4) -> rule2)) -> rule4)) -> rule3)) -> rule5)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
triple5
((triple6) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple6
Fiona is young.
("Fiona" "is" "young" "+")
triple7
((triple5 ((triple6 ((triple6) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
((((triple6) -> (rule6 % int4)) ((triple6 ((triple6) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
((triple4) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple4) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple6 triple7) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple6 ((triple5 ((triple6 ((triple6) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % 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" "+")
int4
((triple6 ((((triple6) -> (rule6 % int5)) ((triple6 ((triple6) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % 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" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
int5
Fiona is green.
("Fiona" "is" "green" "+")
((triple6) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple4 ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple6 ((triple6) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((triple6 triple7) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((((triple6 ((triple5 ((triple6 ((triple6) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is green.
("Fiona" "is" "green" "+")
int5
((((triple6 ((((triple6) -> (rule6 % int6)) ((triple6 ((triple6) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is green.
("Fiona" "is" "green" "+")
int5
Fiona is big.
("Fiona" "is" "big" "+")
int6
Erin is young.
("Erin" "is" "young" "+")
((((triple4) -> (rule6 % int4)) ((triple4 ((triple4) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
((triple4 ((((triple4) -> (rule6 % int5)) ((triple4 ((triple4) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
int5
Erin is white.
("Erin" "is" "white" "+")
((((triple4 ((((triple4) -> (rule6 % int6)) ((triple4 ((triple4) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
int5
Erin is big.
("Erin" "is" "big" "+")
int6