Bob is big. Bob is red. Bob is young. Dave is white. Gary is nice. Gary is quiet. Harry is red. Big, red people are young. If someone is red then they are green. All quiet people are big. If someone is green and not white then they are big. If Harry is nice then Harry is quiet. All young people are nice. If someone is quiet then they are nice. If someone is white then they are red. All red, green people are quiet.
Bob is big.
("Bob" "is" "big" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Big, red people are young.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is red then they are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
All quiet people are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
If someone is green and not white then they are big.
((("someone" "is" "green" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "big" "+"))
If Harry is nice then Harry is quiet.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "quiet" "+"))
All young people are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If someone is quiet then they are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If someone is white then they are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
All red, green people are quiet.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
Gary is quiet.
True
1
proof
[(triple6)]
("Gary" "is" "quiet" "+")
triple6
Bob is not red.
False
1
inv-proof
[(triple2)]
("Bob" "is" "red" "-")
triple2
Dave is red.
True
2
proof
[(((triple4) -> rule8))]
("Dave" "is" "red" "+")
((triple4) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Gary is not big.
False
2
inv-proof
[(((triple6) -> rule3))]
("Gary" "is" "big" "-")
((triple6) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Bob is quiet.
True
4
proof
[(((triple2 ((triple2) -> rule2)) -> rule9))]
("Bob" "is" "quiet" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule9 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not quiet.
False
4
inv-proof
[(((triple2 ((triple2) -> rule2)) -> rule9))]
("Bob" "is" "quiet" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule9 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Harry is nice.
True
5
proof
[(((((triple7 ((triple7) -> rule2)) -> rule9)) -> rule7) OR ((((((((triple7 ((triple7) -> rule2)) -> rule9)) -> rule3) triple7) -> rule1)) -> rule6))]
("Harry" "is" "nice" "+")
((((triple7 ((triple7) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((((triple7 ((triple7) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule3 % int3)) triple7) -> (rule1 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is green.
("Harry" "is" "green" "+")
int5
Harry is not big.
False
5
inv-proof
[(((((triple7 ((triple7) -> rule2)) -> rule9)) -> rule3))]
("Harry" "is" "big" "-")
((((triple7 ((triple7) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Dave is nice.
True
7
proof
[(((((((triple4) -> rule8) ((((triple4) -> rule8)) -> rule2)) -> rule9)) -> rule7) OR ((((((((((triple4) -> rule8) ((((triple4) -> rule8)) -> rule2)) -> rule9)) -> rule3) ((triple4) -> rule8)) -> rule1)) -> rule6))]
("Dave" "is" "nice" "+")
((((((triple4) -> (rule8 % int4)) ((((triple4) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
((((((((((triple4) -> (rule8 % int6)) ((((triple4) -> (rule8 % int6))) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule3 % int3)) ((triple4) -> (rule8 % int6))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
int5
Dave is red.
("Dave" "is" "red" "+")
int6
Dave is not big.
False
7
inv-proof
[(((((((triple4) -> rule8) ((((triple4) -> rule8)) -> rule2)) -> rule9)) -> rule3))]
("Dave" "is" "big" "-")
((((((triple4) -> (rule8 % int4)) ((((triple4) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is young.
True
10
proof
[(((((((((triple4) -> rule8) ((((triple4) -> rule8)) -> rule2)) -> rule9)) -> rule3) ((triple4) -> rule8)) -> rule1))]
("Dave" "is" "young" "+")
((((((((triple4) -> (rule8 % int5)) ((((triple4) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule3 % int2)) ((triple4) -> (rule8 % int5))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
int5
Dave is not young.
False
10
inv-proof
[(((((((((triple4) -> rule8) ((((triple4) -> rule8)) -> rule2)) -> rule9)) -> rule3) ((triple4) -> rule8)) -> rule1))]
("Dave" "is" "young" "-")
((((((((triple4) -> (rule8 % int5)) ((((triple4) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule3 % int2)) ((triple4) -> (rule8 % int5))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
int5
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is young.
Unknown
rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("Gary" "is" "young" "+")
Gary is not green.
Unknown
inv-rconc
[@2: Gary is green.[CWA. Example of deepest failure = (rule2 <- rule8 <- FAIL)]]
("Gary" "is" "green" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Bob is big.[(triple1 OR ((((triple2 ((triple2) -> rule2)) -> rule9)) -> rule3))] Bob is red.[(triple2)] Bob is young.[(triple3 OR ((triple1 triple2) -> rule1) OR ((((((triple2 ((triple2) -> rule2)) -> rule9)) -> rule3) triple2) -> rule1))] Dave is white.[(triple4)] Gary is nice.[(triple5 OR ((triple6) -> rule7))] Gary is quiet.[(triple6)] Harry is red.[(triple7)] @1: Bob is green.[(((triple2) -> rule2))] Bob is nice.[(((triple3) -> rule6) OR ((((triple1 triple2) -> rule1)) -> rule6) OR ((((triple2 ((triple2) -> rule2)) -> rule9)) -> rule7) OR ((((((((triple2 ((triple2) -> rule2)) -> rule9)) -> rule3) triple2) -> rule1)) -> rule6))] Dave is red.[(((triple4) -> rule8))] Gary is big.[(((triple6) -> rule3))] Harry is green.[(((triple7) -> rule2))] @2: Bob is quiet.[(((triple2 ((triple2) -> rule2)) -> rule9))] Dave is green.[(((((triple4) -> rule8)) -> rule2))] Harry is quiet.[(((triple7 ((triple7) -> rule2)) -> rule9))] @3: Dave is quiet.[(((((triple4) -> rule8) ((((triple4) -> rule8)) -> rule2)) -> rule9))] Harry is big.[(((((triple7 ((triple7) -> rule2)) -> rule9)) -> rule3))] Harry is nice.[(((((triple7 ((triple7) -> rule2)) -> rule9)) -> rule7) OR ((((((((triple7 ((triple7) -> rule2)) -> rule9)) -> rule3) triple7) -> rule1)) -> rule6))] @4: Dave is big.[(((((((triple4) -> rule8) ((((triple4) -> rule8)) -> rule2)) -> rule9)) -> rule3))] Dave is nice.[(((((((triple4) -> rule8) ((((triple4) -> rule8)) -> rule2)) -> rule9)) -> rule7) OR ((((((((((triple4) -> rule8) ((((triple4) -> rule8)) -> rule2)) -> rule9)) -> rule3) ((triple4) -> rule8)) -> rule1)) -> rule6))] Harry is young.[(((((((triple7 ((triple7) -> rule2)) -> rule9)) -> rule3) triple7) -> rule1))] @5: Dave is young.[(((((((((triple4) -> rule8) ((((triple4) -> rule8)) -> rule2)) -> rule9)) -> rule3) ((triple4) -> rule8)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
((triple1 triple2) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((((triple2 ((triple2) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
triple4
Gary is nice.
("Gary" "is" "nice" "+")
triple5
((triple6) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Harry is red.
("Harry" "is" "red" "+")
triple7
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple3) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple1 triple2) -> (rule1 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((((((triple2 ((triple2) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule3 % int3)) triple2) -> (rule1 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5
Dave is red.
("Dave" "is" "red" "+")
((triple4) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple6) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple7) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule9 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((triple4) -> (rule8 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple7 ((triple7) -> (rule2 % int2))) -> (rule9 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple4) -> (rule8 % int3)) ((((triple4) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
((((triple7 ((triple7) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((((triple7 ((triple7) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((((triple7 ((triple7) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule3 % int3)) triple7) -> (rule1 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is green.
("Harry" "is" "green" "+")
int5
Dave is big.
("Dave" "is" "big" "+")
((((((triple4) -> (rule8 % int4)) ((((triple4) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
((((((triple4) -> (rule8 % int4)) ((((triple4) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
((((((((((triple4) -> (rule8 % int6)) ((((triple4) -> (rule8 % int6))) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule3 % int3)) ((triple4) -> (rule8 % int6))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
int5
Dave is red.
("Dave" "is" "red" "+")
int6
Harry is young.
("Harry" "is" "young" "+")
((((((triple7 ((triple7) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule3 % int2)) triple7) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
((((((((triple4) -> (rule8 % int5)) ((((triple4) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule3 % int2)) ((triple4) -> (rule8 % int5))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
int5