Bob is young. Charlie is green. Charlie is rough. Charlie is round. Erin is quiet. Erin is round. Gary is green. Gary is quiet. Gary is round. Gary is white. Round things are young. All quiet, white things are green. All quiet, rough things are white. If Charlie is white and Charlie is green then Charlie is round. If Gary is young then Gary is round. Young, green things are rough. All green, young things are big. Quiet, young things are rough.
Bob is young.
("Bob" "is" "young" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
Round things are young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
All quiet, white things are green.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
All quiet, rough things are white.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If Charlie is white and Charlie is green then Charlie is round.
((("Charlie" "is" "white" "+") ("Charlie" "is" "green" "+")) -> ("Charlie" "is" "round" "+"))
If Gary is young then Gary is round.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "round" "+"))
Young, green things are rough.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
All green, young things are big.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Quiet, young things are rough.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Gary is quiet.
True
1
proof
[(triple8)]
("Gary" "is" "quiet" "+")
triple8
Erin is not round.
False
1
inv-proof
[(triple6)]
("Erin" "is" "round" "-")
triple6
Erin is young.
True
2
proof
[(((triple6) -> rule1))]
("Erin" "is" "young" "+")
((triple6) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not young.
False
2
inv-proof
[(((triple6) -> rule1))]
("Erin" "is" "young" "-")
((triple6) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Charlie is big.
True
4
proof
[(((triple2 ((triple4) -> rule1)) -> rule7))]
("Charlie" "is" "big" "+")
((triple2 ((triple4) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Gary is not big.
False
4
inv-proof
[(((triple7 ((triple9) -> rule1)) -> rule7) OR ((((triple8 triple10) -> rule2) ((triple9) -> rule1)) -> rule7) OR ((((triple8 ((triple8 ((triple8 ((triple9) -> rule1)) -> rule8)) -> rule3)) -> rule2) ((triple9) -> rule1)) -> rule7))]
("Gary" "is" "big" "-")
((triple7 ((triple9) -> (rule1 % int2))) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple8 triple10) -> (rule2 % int3)) ((triple9) -> (rule1 % int2))) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((triple8 ((triple8 ((triple8 ((triple9) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) ((triple9) -> (rule1 % int5))) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is young.
("Gary" "is" "young" "+")
int5
Erin is white.
True
6
proof
[(((triple5 ((triple5 ((triple6) -> rule1)) -> rule8)) -> rule3))]
("Erin" "is" "white" "+")
((triple5 ((triple5 ((triple6) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is not white.
False
6
inv-proof
[(((triple5 ((triple5 ((triple6) -> rule1)) -> rule8)) -> rule3))]
("Erin" "is" "white" "-")
((triple5 ((triple5 ((triple6) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is green.
True
8
proof
[(((triple5 ((triple5 ((triple5 ((triple6) -> rule1)) -> rule8)) -> rule3)) -> rule2))]
("Erin" "is" "green" "+")
((triple5 ((triple5 ((triple5 ((triple6) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is not green.
False
8
inv-proof
[(((triple5 ((triple5 ((triple5 ((triple6) -> rule1)) -> rule8)) -> rule3)) -> rule2))]
("Erin" "is" "green" "-")
((triple5 ((triple5 ((triple5 ((triple6) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is big.
True
11
proof
[(((((triple5 ((triple5 ((triple5 ((triple6) -> rule1)) -> rule8)) -> rule3)) -> rule2) ((triple6) -> rule1)) -> rule7))]
("Erin" "is" "big" "+")
((((triple5 ((triple5 ((triple5 ((triple6) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) ((triple6) -> (rule1 % int5))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
int5
Erin is not big.
False
11
inv-proof
[(((((triple5 ((triple5 ((triple5 ((triple6) -> rule1)) -> rule8)) -> rule3)) -> rule2) ((triple6) -> rule1)) -> rule7))]
("Erin" "is" "big" "-")
((((triple5 ((triple5 ((triple5 ((triple6) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) ((triple6) -> (rule1 % int5))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
int5
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "white" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "white" "+")
Bob is not rough.
Unknown
inv-rconc
[@2: Bob is rough.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "green" "+")
Bob is not big.
Unknown
inv-rconc
[@2: Bob is big.[CWA. Example of deepest failure = (rule7 <- rule2 <- FAIL)]]
("Bob" "is" "big" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is young.[(triple1)] Charlie is green.[(triple2)] Charlie is rough.[(triple3 OR ((((triple4) -> rule1) triple2) -> rule6))] Charlie is round.[(triple4)] Erin is quiet.[(triple5)] Erin is round.[(triple6)] Gary is green.[(triple7 OR ((triple8 triple10) -> rule2) OR ((triple8 ((triple8 ((triple8 ((triple9) -> rule1)) -> rule8)) -> rule3)) -> rule2))] Gary is quiet.[(triple8)] Gary is round.[(triple9)] Gary is white.[(triple10 OR ((triple8 ((triple8 ((triple9) -> rule1)) -> rule8)) -> rule3) OR ((triple8 ((((triple9) -> rule1) triple7) -> rule6)) -> rule3))] @1: Charlie is young.[(((triple4) -> rule1))] Erin is young.[(((triple6) -> rule1))] Gary is young.[(((triple9) -> rule1))] @2: Charlie is big.[(((triple2 ((triple4) -> rule1)) -> rule7))] Erin is rough.[(((triple5 ((triple6) -> rule1)) -> rule8))] Gary is big.[(((triple7 ((triple9) -> rule1)) -> rule7) OR ((((triple8 triple10) -> rule2) ((triple9) -> rule1)) -> rule7) OR ((((triple8 ((triple8 ((triple8 ((triple9) -> rule1)) -> rule8)) -> rule3)) -> rule2) ((triple9) -> rule1)) -> rule7))] Gary is rough.[(((triple8 ((triple9) -> rule1)) -> rule8) OR ((((triple9) -> rule1) triple7) -> rule6) OR ((((triple9) -> rule1) ((triple8 triple10) -> rule2)) -> rule6))] @3: Erin is white.[(((triple5 ((triple5 ((triple6) -> rule1)) -> rule8)) -> rule3))] @4: Erin is green.[(((triple5 ((triple5 ((triple5 ((triple6) -> rule1)) -> rule8)) -> rule3)) -> rule2))] @5: Erin is big.[(((((triple5 ((triple5 ((triple5 ((triple6) -> rule1)) -> rule8)) -> rule3)) -> rule2) ((triple6) -> rule1)) -> rule7))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
((((triple4) -> (rule1 % int2)) triple2) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
Erin is round.
("Erin" "is" "round" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
((triple8 triple10) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple8 ((triple8 ((triple8 ((triple9) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
((triple8 ((triple8 ((triple9) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
((triple8 ((((triple9) -> (rule1 % int3)) triple7) -> (rule6 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
((triple4) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple6) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple9) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple2 ((triple4) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((triple5 ((triple6) -> (rule1 % int2))) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((triple7 ((triple9) -> (rule1 % int2))) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple8 triple10) -> (rule2 % int3)) ((triple9) -> (rule1 % int2))) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((triple8 ((triple8 ((triple8 ((triple9) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) ((triple9) -> (rule1 % int5))) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is young.
("Gary" "is" "young" "+")
int5
Gary is rough.
("Gary" "is" "rough" "+")
((triple8 ((triple9) -> (rule1 % int2))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple9) -> (rule1 % int2)) triple7) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple9) -> (rule1 % int3)) ((triple8 triple10) -> (rule2 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((triple5 ((triple5 ((triple6) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
((triple5 ((triple5 ((triple5 ((triple6) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
((((triple5 ((triple5 ((triple5 ((triple6) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) ((triple6) -> (rule1 % int5))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
int5