Bob is big. Harry is blue. If Harry is smart then Harry is big. If something is kind then it is rough. All nice, smart things are rough. If something is smart then it is nice. Blue things are smart. Round, big things are blue. If Harry is big then Harry is blue. If something is smart then it is nice.
Bob is big.
("Bob" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If Harry is smart then Harry is big.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "big" "+"))
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
All nice, smart things are rough.
((("something" "is" "nice" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is smart then it is nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
Round, big things are blue.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If Harry is big then Harry is blue.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "blue" "+"))
If something is smart then it is nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Harry is blue.
True
1
proof
[(triple2)]
("Harry" "is" "blue" "+")
triple2
Harry is not blue.
False
1
inv-proof
[(triple2)]
("Harry" "is" "blue" "-")
triple2
Harry is smart.
True
2
proof
[(((triple2) -> rule5))]
("Harry" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple2) -> rule5))]
("Harry" "is" "smart" "-")
((triple2) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
True
3
proof
[(((((triple2) -> rule5)) -> rule4) OR ((((triple2) -> rule5)) -> rule8))]
("Harry" "is" "nice" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not nice.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule4) OR ((((triple2) -> rule5)) -> rule8))]
("Harry" "is" "nice" "-")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
True
6
proof
[(((((((triple2) -> rule5)) -> rule4) ((triple2) -> rule5)) -> rule3) OR ((((((triple2) -> rule5)) -> rule8) ((triple2) -> rule5)) -> rule3))]
("Harry" "is" "rough" "+")
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2)) ((triple2) -> (rule5 % int3))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((triple2) -> (rule5 % int3))) -> (rule8 % int2)) ((triple2) -> (rule5 % int3))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not rough.
False
6
inv-proof
[(((((((triple2) -> rule5)) -> rule4) ((triple2) -> rule5)) -> rule3) OR ((((((triple2) -> rule5)) -> rule8) ((triple2) -> rule5)) -> rule3))]
("Harry" "is" "rough" "-")
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2)) ((triple2) -> (rule5 % int3))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((triple2) -> (rule5 % int3))) -> (rule8 % int2)) ((triple2) -> (rule5 % int3))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is nice.
Unknown
rconc
[@3: Bob is nice.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule6 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not rough.
Unknown
inv-rconc
[@3: Bob is rough.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule6 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is smart.
Unknown
rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Bob" "is" "smart" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Bob is big.[(triple1)] Harry is blue.[(triple2)] @1: Harry is smart.[(((triple2) -> rule5))] @2: Harry is big.[(((((triple2) -> rule5)) -> rule1))] Harry is nice.[(((((triple2) -> rule5)) -> rule4) OR ((((triple2) -> rule5)) -> rule8))] @3: Harry is rough.[(((((((triple2) -> rule5)) -> rule4) ((triple2) -> rule5)) -> rule3) OR ((((((triple2) -> rule5)) -> rule8) ((triple2) -> rule5)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Harry is blue.
("Harry" "is" "blue" "+")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2)) ((triple2) -> (rule5 % int3))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((triple2) -> (rule5 % int3))) -> (rule8 % int2)) ((triple2) -> (rule5 % int3))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3