Bob is big. Bob is kind. Bob is white. Dave is kind. Dave is smart. Harry is big. Harry is kind. Harry is rough. Harry is smart. Harry is white. If something is rough then it is not cold. If something is cold then it is kind. All smart things are rough. If something is rough and nice then it is not white. If something is rough then it is white. Nice, rough things are white. If Harry is kind then Harry is white. If something is nice then it is big.
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is rough then it is not cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "-"))
If something is cold then it is kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
All smart things are rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is rough and nice then it is not white.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "-"))
If something is rough then it is white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
Nice, rough things are white.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If Harry is kind then Harry is white.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "white" "+"))
If something is nice then it is big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Harry is kind.
True
1
proof
[(triple7)]
("Harry" "is" "kind" "+")
triple7
Dave is not smart.
False
1
inv-proof
[(triple5)]
("Dave" "is" "smart" "-")
triple5
Dave is rough.
True
2
proof
[(((triple5) -> rule3))]
("Dave" "is" "rough" "+")
((triple5) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple5) -> rule3))]
("Dave" "is" "rough" "-")
((triple5) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not cold.
True
3
proof
[(((((triple5) -> rule3)) -> rule1))]
("Dave" "is" "cold" "-")
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not white.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule5))]
("Dave" "is" "white" "-")
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "big" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "rough" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is big.[(triple1)] Bob is kind.[(triple2)] Bob is white.[(triple3)] Dave is kind.[(triple4)] Dave is smart.[(triple5)] Harry is big.[(triple6)] Harry is kind.[(triple7)] Harry is rough.[(triple8 OR ((triple9) -> rule3))] Harry is smart.[(triple9)] Harry is white.[(triple10 OR ((triple7) -> rule7) OR ((triple8) -> rule5) OR ((((triple9) -> rule3)) -> rule5))] @1: Dave is rough.[(((triple5) -> rule3))] Harry is not cold.[(((triple8) -> rule1) OR ((((triple9) -> rule3)) -> rule1))] @2: Dave is not cold.[(((((triple5) -> rule3)) -> rule1))] Dave is white.[(((((triple5) -> rule3)) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Harry is rough.
("Harry" "is" "rough" "+")
triple8
((triple9) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
((triple7) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple8) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((triple5) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
((triple8) -> (rule1 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Dave is not cold.
("Dave" "is" "cold" "-")
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2