Bob is blue. Dave is big. Gary is not blue. Harry is round. If something is young and smart then it is rough. Nice things are rough. If something is big then it is nice. Big things are nice. If something is rough then it is smart. All rough things are young.
Bob is blue.
("Bob" "is" "blue" "+")
Dave is big.
("Dave" "is" "big" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Harry is round.
("Harry" "is" "round" "+")
If something is young and smart then it is rough.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
Nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If something is big then it is nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If something is rough then it is smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
All rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Dave is big.
True
1
proof
[(triple2)]
("Dave" "is" "big" "+")
triple2
Gary is blue.
False
1
inv-proof
[(triple3)]
("Gary" "is" "blue" "+")
triple3
Dave is nice.
True
2
proof
[(((triple2) -> rule3) OR ((triple2) -> rule4))]
("Dave" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple2) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple2) -> rule3) OR ((triple2) -> rule4))]
("Dave" "is" "nice" "-")
((triple2) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple2) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
True
3
proof
[(((((triple2) -> rule3)) -> rule2) OR ((((triple2) -> rule4)) -> rule2))]
("Dave" "is" "rough" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2) OR ((((triple2) -> rule4)) -> rule2))]
("Dave" "is" "rough" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is smart.
True
4
proof
[(((((((triple2) -> rule3)) -> rule2)) -> rule5) OR ((((((triple2) -> rule4)) -> rule2)) -> rule5))]
("Dave" "is" "smart" "+")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is not smart.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule2)) -> rule5) OR ((((((triple2) -> rule4)) -> rule2)) -> rule5))]
("Dave" "is" "smart" "-")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Gary is not young.
Unknown
inv-rconc
[@3: Gary is young.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule3 <- FAIL)]]
("Gary" "is" "young" "-")
Gary is nice.
Unknown
rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "nice" "+")
Gary is not rough.
Unknown
inv-rconc
[@4: Gary is rough.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule2 <- rule3 <- FAIL)]]
("Gary" "is" "rough" "-")
Harry is smart.
Unknown
rconc
[@3: Harry is smart.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule3 <- FAIL)]]
("Harry" "is" "smart" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is blue.[(triple1)] Dave is big.[(triple2)] Gary is not blue.[(triple3)] Harry is round.[(triple4)] @1: Dave is nice.[(((triple2) -> rule3) OR ((triple2) -> rule4))] @2: Dave is rough.[(((((triple2) -> rule3)) -> rule2) OR ((((triple2) -> rule4)) -> rule2))] @3: Dave is smart.[(((((((triple2) -> rule3)) -> rule2)) -> rule5) OR ((((((triple2) -> rule4)) -> rule2)) -> rule5))] Dave is young.[(((((((triple2) -> rule3)) -> rule2)) -> rule6) OR ((((((triple2) -> rule4)) -> rule2)) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Gary is not blue.
("Gary" "is" "blue" "-")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple2) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3