Bob is kind. Charlie is not blue. Charlie is green. Charlie is not white. Dave is big. Gary is big. Gary is round. All green, kind people are smart. If someone is big and kind then they are round. Smart, green people are big. If someone is blue and not kind then they are green. If someone is kind then they are green. If someone is round then they are not white. If Dave is white and Dave is not big then Dave is round.
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Dave is big.
("Dave" "is" "big" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is round.
("Gary" "is" "round" "+")
All green, kind people are smart.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is big and kind then they are round.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
Smart, green people are big.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone is blue and not kind then they are green.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "green" "+"))
If someone is kind then they are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If someone is round then they are not white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "-"))
If Dave is white and Dave is not big then Dave is round.
((("Dave" "is" "white" "+") ("Dave" "is" "big" "~")) -> ("Dave" "is" "round" "+"))
Bob is kind.
True
1
proof
[(triple1)]
("Bob" "is" "kind" "+")
triple1
Dave is not big.
False
1
inv-proof
[(triple5)]
("Dave" "is" "big" "-")
triple5
Bob is green.
True
2
proof
[(((triple1) -> rule5))]
("Bob" "is" "green" "+")
((triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Gary is white.
False
2
inv-proof
[(((triple7) -> rule6))]
("Gary" "is" "white" "+")
((triple7) -> (rule6 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Bob is smart.
True
4
proof
[(((((triple1) -> rule5) triple1) -> rule1))]
("Bob" "is" "smart" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not smart.
False
4
inv-proof
[(((((triple1) -> rule5) triple1) -> rule1))]
("Bob" "is" "smart" "-")
((((triple1) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is big.
True
7
proof
[(((((((triple1) -> rule5) triple1) -> rule1) ((triple1) -> rule5)) -> rule3))]
("Bob" "is" "big" "+")
((((((triple1) -> (rule5 % int3)) triple1) -> (rule1 % int2)) ((triple1) -> (rule5 % int3))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not big.
False
7
inv-proof
[(((((((triple1) -> rule5) triple1) -> rule1) ((triple1) -> rule5)) -> rule3))]
("Bob" "is" "big" "-")
((((((triple1) -> (rule5 % int3)) triple1) -> (rule1 % int2)) ((triple1) -> (rule5 % int3))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is round.
True
9
proof
[(((((((((triple1) -> rule5) triple1) -> rule1) ((triple1) -> rule5)) -> rule3) triple1) -> rule2))]
("Bob" "is" "round" "+")
((((((((triple1) -> (rule5 % int4)) triple1) -> (rule1 % int3)) ((triple1) -> (rule5 % int4))) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is not round.
False
9
inv-proof
[(((((((((triple1) -> rule5) triple1) -> rule1) ((triple1) -> rule5)) -> rule3) triple1) -> rule2))]
("Bob" "is" "round" "-")
((((((((triple1) -> (rule5 % int4)) triple1) -> (rule1 % int3)) ((triple1) -> (rule5 % int4))) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is not white.
True
10
proof
[(((((((((((triple1) -> rule5) triple1) -> rule1) ((triple1) -> rule5)) -> rule3) triple1) -> rule2)) -> rule6))]
("Bob" "is" "white" "-")
((((((((((triple1) -> (rule5 % int5)) triple1) -> (rule1 % int4)) ((triple1) -> (rule5 % int5))) -> (rule3 % int3)) triple1) -> (rule2 % int2))) -> (rule6 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5
Bob is white.
False
10
inv-proof
[(((((((((((triple1) -> rule5) triple1) -> rule1) ((triple1) -> rule5)) -> rule3) triple1) -> rule2)) -> rule6))]
("Bob" "is" "white" "+")
((((((((((triple1) -> (rule5 % int5)) triple1) -> (rule1 % int4)) ((triple1) -> (rule5 % int5))) -> (rule3 % int3)) triple1) -> (rule2 % int2))) -> (rule6 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "green" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "green" "+")
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "smart" "-")
Dave is round.
Unknown
rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "round" "+")
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "smart" "-")
Charlie is round.
Unknown
rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "round" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Bob is kind.[(triple1)] Charlie is green.[(triple3)] Charlie is not blue.[(triple2)] Charlie is not white.[(triple4)] Dave is big.[(triple5)] Gary is big.[(triple6)] Gary is round.[(triple7)] @1: Bob is green.[(((triple1) -> rule5))] Gary is not white.[(((triple7) -> rule6))] @2: Bob is smart.[(((((triple1) -> rule5) triple1) -> rule1))] @3: Bob is big.[(((((((triple1) -> rule5) triple1) -> rule1) ((triple1) -> rule5)) -> rule3))] @4: Bob is round.[(((((((((triple1) -> rule5) triple1) -> rule1) ((triple1) -> rule5)) -> rule3) triple1) -> rule2))] @5: Bob is not white.[(((((((((((triple1) -> rule5) triple1) -> rule1) ((triple1) -> rule5)) -> rule3) triple1) -> rule2)) -> rule6))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple2
Charlie is not white.
("Charlie" "is" "white" "-")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Gary is not white.
("Gary" "is" "white" "-")
((triple7) -> (rule6 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((((((triple1) -> (rule5 % int3)) triple1) -> (rule1 % int2)) ((triple1) -> (rule5 % int3))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
((((((((triple1) -> (rule5 % int4)) triple1) -> (rule1 % int3)) ((triple1) -> (rule5 % int4))) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is not white.
("Bob" "is" "white" "-")
((((((((((triple1) -> (rule5 % int5)) triple1) -> (rule1 % int4)) ((triple1) -> (rule5 % int5))) -> (rule3 % int3)) triple1) -> (rule2 % int2))) -> (rule6 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5