Bob is nice. Dave is smart. Erin is nice. Gary is rough. If Dave is smart then Dave is green. Smart, green people are big. All quiet people are furry. All quiet, green people are furry. Big, quiet people are smart. If someone is big then they are quiet.
Bob is nice.
("Bob" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If Dave is smart then Dave is green.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "green" "+"))
Smart, green people are big.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
All quiet people are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
All quiet, green people are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
Big, quiet people are smart.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If someone is big then they are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
Dave is smart.
True
1
proof
[(triple2)]
("Dave" "is" "smart" "+")
triple2
Gary is not rough.
False
1
inv-proof
[(triple4)]
("Gary" "is" "rough" "-")
triple4
Dave is green.
True
2
proof
[(((triple2) -> rule1))]
("Dave" "is" "green" "+")
((triple2) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple2) -> rule1))]
("Dave" "is" "green" "-")
((triple2) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
True
4
proof
[(((triple2 ((triple2) -> rule1)) -> rule2))]
("Dave" "is" "big" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not big.
False
4
inv-proof
[(((triple2 ((triple2) -> rule1)) -> rule2))]
("Dave" "is" "big" "-")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
True
5
proof
[(((((triple2 ((triple2) -> rule1)) -> rule2)) -> rule6))]
("Dave" "is" "quiet" "+")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is not quiet.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule1)) -> rule2)) -> rule6))]
("Dave" "is" "quiet" "-")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@2: Bob is quiet.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is smart.
Unknown
rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Bob" "is" "smart" "+")
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "big" "-")
Gary is furry.
Unknown
rconc
[@3: Gary is furry.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule2 <- FAIL)]]
("Gary" "is" "furry" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Bob is nice.[(triple1)] Dave is smart.[(triple2)] Erin is nice.[(triple3)] Gary is rough.[(triple4)] @1: Dave is green.[(((triple2) -> rule1))] @2: Dave is big.[(((triple2 ((triple2) -> rule1)) -> rule2))] @3: Dave is quiet.[(((((triple2 ((triple2) -> rule1)) -> rule2)) -> rule6))] @4: Dave is furry.[(((((((triple2 ((triple2) -> rule1)) -> rule2)) -> rule6)) -> rule3) OR ((((((triple2 ((triple2) -> rule1)) -> rule2)) -> rule6) ((triple2) -> rule1)) -> rule4))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Gary is rough.
("Gary" "is" "rough" "+")
triple4
Dave is green.
("Dave" "is" "green" "+")
((triple2) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
((((((triple2 ((triple2) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
((((((triple2 ((triple2) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule6 % int2)) ((triple2) -> (rule1 % int4))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4