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