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