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