Anne is big. Anne is green. Anne is rough. Bob is furry. Bob is not rough. Charlie is green. Charlie is young. Harry is big. Harry is green. Harry is not red. If someone is big then they are not smart. If someone is big and not smart then they are furry. All furry people are not young. If Harry is young and Harry is red then Harry is not rough. All red, young people are green. All rough people are green.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is not red.
("Harry" "is" "red" "-")
If someone is big then they are not smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "-"))
If someone is big and not smart then they are furry.
((("someone" "is" "big" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "furry" "+"))
All furry people are not young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "-"))
If Harry is young and Harry is red then Harry is not rough.
((("Harry" "is" "young" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "rough" "-"))
All red, young people are green.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
All rough people are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
Anne is rough.
True
1
proof
[(triple3)]
("Anne" "is" "rough" "+")
triple3
Bob is rough.
False
1
inv-proof
[(triple5)]
("Bob" "is" "rough" "+")
triple5
Anne is not smart.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "smart" "-")
((triple1) -> (rule1 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Harry is smart.
False
2
inv-proof
[(((triple8) -> rule1))]
("Harry" "is" "smart" "+")
((triple8) -> (rule1 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is furry.
True
4
proof
[(((triple8 ((triple8) -> rule1)) -> rule2))]
("Harry" "is" "furry" "+")
((triple8 ((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not smart.
("Harry" "is" "smart" "-")
int2
Anne is not furry.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule2))]
("Anne" "is" "furry" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not smart.
("Anne" "is" "smart" "-")
int2
Anne is not young.
True
5
proof
[(((((triple1 ((triple1) -> rule1)) -> rule2)) -> rule3))]
("Anne" "is" "young" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not smart.
("Anne" "is" "smart" "-")
int3
Harry is young.
False
5
inv-proof
[(((((triple8 ((triple8) -> rule1)) -> rule2)) -> rule3))]
("Harry" "is" "young" "+")
((((triple8 ((triple8) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not smart.
("Harry" "is" "smart" "-")
int3
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "furry" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "green" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is green.[(triple2 OR ((triple3) -> rule6))] Anne is rough.[(triple3)] Bob is furry.[(triple4)] Bob is not rough.[(triple5)] Charlie is green.[(triple6)] Charlie is young.[(triple7)] Harry is big.[(triple8)] Harry is green.[(triple9)] Harry is not red.[(triple10)] @1: Anne is not smart.[(((triple1) -> rule1))] Bob is not young.[(((triple4) -> rule3))] Harry is not smart.[(((triple8) -> rule1))] @2: Anne is furry.[(((triple1 ((triple1) -> rule1)) -> rule2))] Harry is furry.[(((triple8 ((triple8) -> rule1)) -> rule2))] @3: Anne is not young.[(((((triple1 ((triple1) -> rule1)) -> rule2)) -> rule3))] Harry is not young.[(((((triple8 ((triple8) -> rule1)) -> rule2)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple3) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
triple4
Bob is not rough.
("Bob" "is" "rough" "-")
triple5
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is not red.
("Harry" "is" "red" "-")
triple10
Anne is not smart.
("Anne" "is" "smart" "-")
((triple1) -> (rule1 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Bob is not young.
("Bob" "is" "young" "-")
((triple4) -> (rule3 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Harry is not smart.
("Harry" "is" "smart" "-")
((triple8) -> (rule1 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not smart.
("Anne" "is" "smart" "-")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((triple8 ((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not smart.
("Harry" "is" "smart" "-")
int2
Anne is not young.
("Anne" "is" "young" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not smart.
("Anne" "is" "smart" "-")
int3
Harry is not young.
("Harry" "is" "young" "-")
((((triple8 ((triple8) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not smart.
("Harry" "is" "smart" "-")
int3