Anne is green. Bob is smart. Fiona is young. Harry is smart. All smart people are round. If someone is green then they are round. Smart, nice people are green. If someone is round and young then they are green. All smart, green people are not nice. All kind people are not rough. If someone is smart then they are kind. All rough people are kind.
Anne is green.
("Anne" "is" "green" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If someone is green then they are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Smart, nice people are green.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone is round and young then they are green.
((("someone" "is" "round" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
All smart, green people are not nice.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "-"))
All kind people are not rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "-"))
If someone is smart then they are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
All rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Fiona is young.
True
1
proof
[(triple3)]
("Fiona" "is" "young" "+")
triple3
Anne is not green.
False
1
inv-proof
[(triple1)]
("Anne" "is" "green" "-")
triple1
Bob is kind.
True
2
proof
[(((triple2) -> rule7))]
("Bob" "is" "kind" "+")
((triple2) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "round" "-")
((triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Harry is not rough.
True
3
proof
[(((((triple4) -> rule7)) -> rule6))]
("Harry" "is" "rough" "-")
((((triple4) -> (rule7 % int2))) -> (rule6 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
False
3
inv-proof
[(((((triple4) -> rule7)) -> rule6))]
("Harry" "is" "rough" "+")
((((triple4) -> (rule7 % int2))) -> (rule6 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "green" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "kind" "+")
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "green" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Anne is green.[(triple1)] Bob is smart.[(triple2)] Fiona is young.[(triple3)] Harry is smart.[(triple4)] @1: Anne is round.[(((triple1) -> rule2))] Bob is kind.[(((triple2) -> rule7))] Bob is round.[(((triple2) -> rule1))] Harry is kind.[(((triple4) -> rule7))] Harry is round.[(((triple4) -> rule1))] @2: Bob is not rough.[(((((triple2) -> rule7)) -> rule6))] Harry is not rough.[(((((triple4) -> rule7)) -> rule6))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Fiona is young.
("Fiona" "is" "young" "+")
triple3
Harry is smart.
("Harry" "is" "smart" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple4) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple4) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Bob is not rough.
("Bob" "is" "rough" "-")
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Harry is not rough.
("Harry" "is" "rough" "-")
((((triple4) -> (rule7 % int2))) -> (rule6 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2