Anne is green. Charlie is rough. Fiona is red. Harry is furry. If something is green and smart then it is red. Red things are green. If Harry is smart and Harry is rough then Harry is red. If Charlie is furry and Charlie is rough then Charlie is green. All quiet, smart things are nice. If something is furry and rough then it is nice. Green things are smart. If something is smart and red then it is furry.
Anne is green.
("Anne" "is" "green" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If something is green and smart then it is red.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If Harry is smart and Harry is rough then Harry is red.
((("Harry" "is" "smart" "+") ("Harry" "is" "rough" "+")) -> ("Harry" "is" "red" "+"))
If Charlie is furry and Charlie is rough then Charlie is green.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "green" "+"))
All quiet, smart things are nice.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If something is furry and rough then it is nice.
((("something" "is" "furry" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
Green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If something is smart and red then it is furry.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Harry is furry.
True
1
proof
[(triple4)]
("Harry" "is" "furry" "+")
triple4
Harry is not furry.
False
1
inv-proof
[(triple4)]
("Harry" "is" "furry" "-")
triple4
Fiona is green.
True
2
proof
[(((triple3) -> rule2))]
("Fiona" "is" "green" "+")
((triple3) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is not green.
False
2
inv-proof
[(((triple3) -> rule2))]
("Fiona" "is" "green" "-")
((triple3) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Anne is red.
True
4
proof
[(((triple1 ((triple1) -> rule7)) -> rule1))]
("Anne" "is" "red" "+")
((triple1 ((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Fiona is not smart.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule7))]
("Fiona" "is" "smart" "-")
((((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "nice" "-")
Charlie is green.
Unknown
rconc
[@4: Charlie is green.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule4 <- rule8 <- FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not nice.
Unknown
inv-rconc
[@4: Charlie is nice.[CWA. Example of deepest failure = (rule6 <- rule8 <- rule1 <- rule2 <- FAIL)]]
("Charlie" "is" "nice" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
@0: Anne is green.[(triple1)] Charlie is rough.[(triple2)] Fiona is red.[(triple3)] Harry is furry.[(triple4)] @1: Anne is smart.[(((triple1) -> rule7))] Fiona is green.[(((triple3) -> rule2))] @2: Anne is red.[(((triple1 ((triple1) -> rule7)) -> rule1))] Fiona is smart.[(((((triple3) -> rule2)) -> rule7))] @3: Anne is furry.[(((((triple1) -> rule7) ((triple1 ((triple1) -> rule7)) -> rule1)) -> rule8))] Fiona is furry.[(((((((triple3) -> rule2)) -> rule7) triple3) -> rule8))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Fiona is red.
("Fiona" "is" "red" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple3) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple1 ((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule7 % int3)) ((triple1 ((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
((((((triple3) -> (rule2 % int3))) -> (rule7 % int2)) triple3) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3