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