Dave is smart. Erin is kind. Erin is quiet. Erin is round. Fiona is kind. Gary is quiet. Gary is round. Round, blue people are quiet. If someone is kind then they are big. Smart people are nice. All smart, nice people are blue. If someone is blue then they are round. If someone is smart and kind then they are big. Round, kind people are big. All big, nice people are kind. Blue, quiet people are kind.
Dave is smart.
("Dave" "is" "smart" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Round, blue people are quiet.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If someone is kind then they are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
All smart, nice people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue then they are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone is smart and kind then they are big.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Round, kind people are big.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
All big, nice people are kind.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
Blue, quiet people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Gary is round.
True
1
proof
[(triple7)]
("Gary" "is" "round" "+")
triple7
Gary is not round.
False
1
inv-proof
[(triple7)]
("Gary" "is" "round" "-")
triple7
Fiona is big.
True
2
proof
[(((triple5) -> rule2))]
("Fiona" "is" "big" "+")
((triple5) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("Dave" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule4))]
("Dave" "is" "blue" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not blue.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule4))]
("Dave" "is" "blue" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is round.
True
5
proof
[(((((triple1 ((triple1) -> rule3)) -> rule4)) -> rule5))]
("Dave" "is" "round" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is not round.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule3)) -> rule4)) -> rule5))]
("Dave" "is" "round" "-")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is quiet.
True
10
proof
[(((((((triple1 ((triple1) -> rule3)) -> rule4)) -> rule5) ((triple1 ((triple1) -> rule3)) -> rule4)) -> rule1))]
("Dave" "is" "quiet" "+")
((((((triple1 ((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2)) ((triple1 ((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is not quiet.
False
10
inv-proof
[(((((((triple1 ((triple1) -> rule3)) -> rule4)) -> rule5) ((triple1 ((triple1) -> rule3)) -> rule4)) -> rule1))]
("Dave" "is" "quiet" "-")
((((((triple1 ((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2)) ((triple1 ((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is kind.
True
15
proof
[(((((triple1 ((triple1) -> rule3)) -> rule4) ((((((triple1 ((triple1) -> rule3)) -> rule4)) -> rule5) ((triple1 ((triple1) -> rule3)) -> rule4)) -> rule1)) -> rule9))]
("Dave" "is" "kind" "+")
((((triple1 ((triple1) -> (rule3 % int5))) -> (rule4 % int4)) ((((((triple1 ((triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3)) ((triple1 ((triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule1 % int2))) -> (rule9 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Dave is not kind.
False
15
inv-proof
[(((((triple1 ((triple1) -> rule3)) -> rule4) ((((((triple1 ((triple1) -> rule3)) -> rule4)) -> rule5) ((triple1 ((triple1) -> rule3)) -> rule4)) -> rule1)) -> rule9))]
("Dave" "is" "kind" "-")
((((triple1 ((triple1) -> (rule3 % int5))) -> (rule4 % int4)) ((((((triple1 ((triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3)) ((triple1 ((triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule1 % int2))) -> (rule9 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Fiona is not round.
Unknown
inv-rconc
[@2: Fiona is round.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is quiet.
Unknown
rconc
[@2: Fiona is quiet.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "nice" "-")
Fiona is blue.
Unknown
rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "blue" "+")
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "nice" "-")
Gary is big.
Unknown
rconc
[@3: Gary is big.[CWA. Example of deepest failure = (rule2 <- rule8 <- rule3 <- FAIL)]]
("Gary" "is" "big" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Dave is smart.[(triple1)] Erin is kind.[(triple2)] Erin is quiet.[(triple3)] Erin is round.[(triple4)] Fiona is kind.[(triple5)] Gary is quiet.[(triple6)] Gary is round.[(triple7)] @1: Dave is nice.[(((triple1) -> rule3))] Erin is big.[(((triple2) -> rule2) OR ((triple4 triple2) -> rule7))] Fiona is big.[(((triple5) -> rule2))] @2: Dave is blue.[(((triple1 ((triple1) -> rule3)) -> rule4))] @3: Dave is round.[(((((triple1 ((triple1) -> rule3)) -> rule4)) -> rule5))] @4: Dave is quiet.[(((((((triple1 ((triple1) -> rule3)) -> rule4)) -> rule5) ((triple1 ((triple1) -> rule3)) -> rule4)) -> rule1))] @5: Dave is kind.[(((((triple1 ((triple1) -> rule3)) -> rule4) ((((((triple1 ((triple1) -> rule3)) -> rule4)) -> rule5) ((triple1 ((triple1) -> rule3)) -> rule4)) -> rule1)) -> rule9))] @6: Dave is big.[(((((((triple1 ((triple1) -> rule3)) -> rule4) ((((((triple1 ((triple1) -> rule3)) -> rule4)) -> rule5) ((triple1 ((triple1) -> rule3)) -> rule4)) -> rule1)) -> rule9)) -> rule2) OR ((triple1 ((((triple1 ((triple1) -> rule3)) -> rule4) ((((((triple1 ((triple1) -> rule3)) -> rule4)) -> rule5) ((triple1 ((triple1) -> rule3)) -> rule4)) -> rule1)) -> rule9)) -> rule6) OR ((((((triple1 ((triple1) -> rule3)) -> rule4)) -> rule5) ((((triple1 ((triple1) -> rule3)) -> rule4) ((((((triple1 ((triple1) -> rule3)) -> rule4)) -> rule5) ((triple1 ((triple1) -> rule3)) -> rule4)) -> rule1)) -> rule9)) -> rule7))]
Dave is smart.
("Dave" "is" "smart" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Erin is round.
("Erin" "is" "round" "+")
triple4
Fiona is kind.
("Fiona" "is" "kind" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
Dave is nice.
("Dave" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple2) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple4 triple2) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple5) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
((((((triple1 ((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2)) ((triple1 ((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
((((triple1 ((triple1) -> (rule3 % int5))) -> (rule4 % int4)) ((((((triple1 ((triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3)) ((triple1 ((triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule1 % int2))) -> (rule9 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Dave is big.
("Dave" "is" "big" "+")
((((((triple1 ((triple1) -> (rule3 % int6))) -> (rule4 % int5)) ((((((triple1 ((triple1) -> (rule3 % int6))) -> (rule4 % int5))) -> (rule5 % int4)) ((triple1 ((triple1) -> (rule3 % int6))) -> (rule4 % int5))) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
int5
Dave is nice.
("Dave" "is" "nice" "+")
int6
((triple1 ((((triple1 ((triple1) -> (rule3 % int6))) -> (rule4 % int5)) ((((((triple1 ((triple1) -> (rule3 % int6))) -> (rule4 % int5))) -> (rule5 % int4)) ((triple1 ((triple1) -> (rule3 % int6))) -> (rule4 % int5))) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
int5
Dave is nice.
("Dave" "is" "nice" "+")
int6
((((((triple1 ((triple1) -> (rule3 % int6))) -> (rule4 % int5))) -> (rule5 % int4)) ((((triple1 ((triple1) -> (rule3 % int6))) -> (rule4 % int5)) ((((((triple1 ((triple1) -> (rule3 % int6))) -> (rule4 % int5))) -> (rule5 % int4)) ((triple1 ((triple1) -> (rule3 % int6))) -> (rule4 % int5))) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
int5
Dave is nice.
("Dave" "is" "nice" "+")
int6