Bob is furry. Bob is kind. Bob is rough. Charlie is big. Charlie is blue. Charlie is furry. Charlie is green. Charlie is kind. Charlie is smart. Dave is blue. Dave is kind. Dave is smart. Big things are blue. All rough things are big. If something is kind then it is big. All blue things are smart. If something is rough then it is kind. All smart things are big.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
All rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is kind then it is big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
All blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If something is rough then it is kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
All smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Dave is smart.
True
1
proof
[(triple12 OR ((triple10) -> rule4) OR ((((((triple11) -> rule3)) -> rule1)) -> rule4))]
("Dave" "is" "smart" "+")
triple12
((triple10) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((((triple11) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Bob is not furry.
False
1
inv-proof
[(triple1)]
("Bob" "is" "furry" "-")
triple1
Bob is big.
True
2
proof
[(((triple2) -> rule3) OR ((triple3) -> rule2) OR ((((triple3) -> rule5)) -> rule3))]
("Bob" "is" "big" "+")
((triple2) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple3) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not big.
False
2
inv-proof
[(((triple2) -> rule3) OR ((triple3) -> rule2) OR ((((triple3) -> rule5)) -> rule3))]
("Bob" "is" "big" "-")
((triple2) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple3) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is blue.
True
3
proof
[(((((triple2) -> rule3)) -> rule1) OR ((((triple3) -> rule2)) -> rule1) OR ((((((triple3) -> rule5)) -> rule3)) -> rule1))]
("Bob" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is not blue.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1) OR ((((triple3) -> rule2)) -> rule1) OR ((((((triple3) -> rule5)) -> rule3)) -> rule1))]
("Bob" "is" "blue" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is smart.
True
4
proof
[(((((((triple2) -> rule3)) -> rule1)) -> rule4) OR ((((((triple3) -> rule2)) -> rule1)) -> rule4) OR ((((((((triple3) -> rule5)) -> rule3)) -> rule1)) -> rule4))]
("Bob" "is" "smart" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((((triple3) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is not smart.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule1)) -> rule4) OR ((((((triple3) -> rule2)) -> rule1)) -> rule4) OR ((((((((triple3) -> rule5)) -> rule3)) -> rule1)) -> rule4))]
("Bob" "is" "smart" "-")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((((triple3) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Bob is furry.[(triple1)] Bob is kind.[(triple2 OR ((triple3) -> rule5))] Bob is rough.[(triple3)] Charlie is big.[(triple4 OR ((triple8) -> rule3) OR ((triple9) -> rule6) OR ((((triple5) -> rule4)) -> rule6))] Charlie is blue.[(triple5 OR ((triple4) -> rule1) OR ((((triple8) -> rule3)) -> rule1) OR ((((triple9) -> rule6)) -> rule1))] Charlie is furry.[(triple6)] Charlie is green.[(triple7)] Charlie is kind.[(triple8)] Charlie is smart.[(triple9 OR ((triple5) -> rule4) OR ((((triple4) -> rule1)) -> rule4) OR ((((((triple8) -> rule3)) -> rule1)) -> rule4))] Dave is blue.[(triple10 OR ((((triple11) -> rule3)) -> rule1) OR ((((triple12) -> rule6)) -> rule1))] Dave is kind.[(triple11)] Dave is smart.[(triple12 OR ((triple10) -> rule4) OR ((((((triple11) -> rule3)) -> rule1)) -> rule4))] @1: Bob is big.[(((triple2) -> rule3) OR ((triple3) -> rule2) OR ((((triple3) -> rule5)) -> rule3))] Dave is big.[(((triple11) -> rule3) OR ((triple12) -> rule6) OR ((((triple10) -> rule4)) -> rule6))] @2: Bob is blue.[(((((triple2) -> rule3)) -> rule1) OR ((((triple3) -> rule2)) -> rule1) OR ((((((triple3) -> rule5)) -> rule3)) -> rule1))] @3: Bob is smart.[(((((((triple2) -> rule3)) -> rule1)) -> rule4) OR ((((((triple3) -> rule2)) -> rule1)) -> rule4) OR ((((((((triple3) -> rule5)) -> rule3)) -> rule1)) -> rule4))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
((triple3) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
((triple8) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple9) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
((triple4) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple8) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple9) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Charlie is green.
("Charlie" "is" "green" "+")
triple7
Charlie is kind.
("Charlie" "is" "kind" "+")
triple8
Charlie is smart.
("Charlie" "is" "smart" "+")
triple9
((triple5) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((((triple8) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
triple10
((((triple11) -> (rule3 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple12) -> (rule6 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
triple11
Dave is smart.
("Dave" "is" "smart" "+")
triple12
((triple10) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((((triple11) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
((triple2) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple3) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((triple11) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple12) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((((triple3) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4