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