Anne is blue. Anne is kind. Anne is nice. Anne is young. Charlie is young. Gary is not nice. Gary is young. Harry is not big. Harry is kind. Harry is nice. Harry is smart. Harry is young. If Gary is blue then Gary is nice. All smart people are rough. Kind people are smart. If someone is young and not smart then they are big. All smart people are nice. If someone is big and not young then they are nice. If someone is rough and not young then they are not nice. If someone is blue and not young then they are nice.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is not nice.
("Gary" "is" "nice" "-")
Gary is young.
("Gary" "is" "young" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If Gary is blue then Gary is nice.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "nice" "+"))
All smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Kind people are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is young and not smart then they are big.
((("someone" "is" "young" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "big" "+"))
All smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If someone is big and not young then they are nice.
((("someone" "is" "big" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "nice" "+"))
If someone is rough and not young then they are not nice.
((("someone" "is" "rough" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "nice" "-"))
If someone is blue and not young then they are nice.
((("someone" "is" "blue" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "nice" "+"))
Charlie is young.
True
1
proof
[(triple5)]
("Charlie" "is" "young" "+")
triple5
Anne is not nice.
False
1
inv-proof
[(triple3 OR ((((triple2) -> rule3)) -> rule5))]
("Anne" "is" "nice" "-")
triple3
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is smart.
True
2
proof
[(((triple2) -> rule3))]
("Anne" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple2) -> rule3))]
("Anne" "is" "smart" "-")
((triple2) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("Anne" "is" "rough" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not rough.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("Anne" "is" "rough" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "big" "+")
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "big" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Anne is blue.[(triple1)] Anne is kind.[(triple2)] Anne is nice.[(triple3 OR ((((triple2) -> rule3)) -> rule5))] Anne is young.[(triple4)] Charlie is young.[(triple5)] Gary is not nice.[(triple6)] Gary is young.[(triple7)] Harry is kind.[(triple9)] Harry is nice.[(triple10 OR ((triple11) -> rule5) OR ((((triple9) -> rule3)) -> rule5))] Harry is not big.[(triple8)] Harry is smart.[(triple11 OR ((triple9) -> rule3))] Harry is young.[(triple12)] @1: Anne is smart.[(((triple2) -> rule3))] Harry is rough.[(((triple11) -> rule2) OR ((((triple9) -> rule3)) -> rule2))] @2: Anne is rough.[(((((triple2) -> rule3)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Gary is not nice.
("Gary" "is" "nice" "-")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
((triple11) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not big.
("Harry" "is" "big" "-")
triple8
Harry is smart.
("Harry" "is" "smart" "+")
triple11
((triple9) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple12
Anne is smart.
("Anne" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple11) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2