Bob is big. Dave is smart. Gary is young. Harry is red. If Bob is nice then Bob is not rough. All smart people are nice. All big, nice people are not red. Big, young people are rough. If Dave is big then Dave is nice. If Bob is young then Bob is not big. If someone is red then they are big. All nice people are big.
Bob is big.
("Bob" "is" "big" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is red.
("Harry" "is" "red" "+")
If Bob is nice then Bob is not rough.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "rough" "-"))
All smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
All big, nice people are not red.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "-"))
Big, young people are rough.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If Dave is big then Dave is nice.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "nice" "+"))
If Bob is young then Bob is not big.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "big" "-"))
If someone is red then they are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
All nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Dave is nice.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "nice" "+")
((triple2) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple4) -> rule7))]
("Harry" "is" "big" "-")
((triple4) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Dave is big.
True
3
proof
[(((((triple2) -> rule2)) -> rule8))]
("Dave" "is" "big" "+")
((((triple2) -> (rule2 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule8))]
("Dave" "is" "big" "-")
((((triple2) -> (rule2 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "nice" "-")
Gary is rough.
Unknown
rconc
[@3: Gary is rough.[CWA. Example of deepest failure = (rule4 <- rule8 <- rule2 <- FAIL)]]
("Gary" "is" "rough" "+")
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "rough" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Bob is big.[(triple1)] Dave is smart.[(triple2)] Gary is young.[(triple3)] Harry is red.[(triple4)] @1: Dave is nice.[(((triple2) -> rule2))] Harry is big.[(((triple4) -> rule7))] @2: Dave is big.[(((((triple2) -> rule2)) -> rule8))] @3: Dave is not red.[(((((((triple2) -> rule2)) -> rule8) ((triple2) -> rule2)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Harry is red.
("Harry" "is" "red" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple4) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple2) -> (rule2 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not red.
("Dave" "is" "red" "-")
((((((triple2) -> (rule2 % int3))) -> (rule8 % int2)) ((triple2) -> (rule2 % int3))) -> (rule3 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3