Anne is big. Anne is kind. Anne is nice. Anne is rough. Anne is white. Fiona is cold. Fiona is not kind. Fiona is nice. Fiona is white. Fiona is young. Rough things are white. All big things are white. If something is nice then it is big. If something is cold and not young then it is big. Big, young things are not rough. Young, rough things are nice. All big, rough things are kind. If Fiona is not big then Fiona is not kind.
Anne is big.
("Anne" "is" "big" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is not kind.
("Fiona" "is" "kind" "-")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Rough things are white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
All big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If something is nice then it is big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is cold and not young then it is big.
((("something" "is" "cold" "+") ("something" "is" "young" "~")) -> ("something" "is" "big" "+"))
Big, young things are not rough.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "-"))
Young, rough things are nice.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All big, rough things are kind.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If Fiona is not big then Fiona is not kind.
((("Fiona" "is" "big" "~")) -> ("Fiona" "is" "kind" "-"))
Fiona is cold.
True
1
proof
[(triple6)]
("Fiona" "is" "cold" "+")
triple6
Anne is not white.
False
1
inv-proof
[(triple5 OR ((triple1) -> rule2) OR ((triple4) -> rule1) OR ((((triple3) -> rule3)) -> rule2))]
("Anne" "is" "white" "-")
triple5
((triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple4) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Fiona is big.
True
2
proof
[(((triple8) -> rule3))]
("Fiona" "is" "big" "+")
((triple8) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not big.
False
2
inv-proof
[(((triple8) -> rule3))]
("Fiona" "is" "big" "-")
((triple8) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not rough.
True
4
proof
[(((((triple8) -> rule3) triple10) -> rule5))]
("Fiona" "is" "rough" "-")
((((triple8) -> (rule3 % int2)) triple10) -> (rule5 % int1))
Fiona is not rough.
("Fiona" "is" "rough" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is rough.
False
4
inv-proof
[(((((triple8) -> rule3) triple10) -> rule5))]
("Fiona" "is" "rough" "+")
((((triple8) -> (rule3 % int2)) triple10) -> (rule5 % int1))
Fiona is not rough.
("Fiona" "is" "rough" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is big.[(triple1 OR ((triple3) -> rule3))] Anne is kind.[(triple2 OR ((triple1 triple4) -> rule7) OR ((((triple3) -> rule3) triple4) -> rule7))] Anne is nice.[(triple3)] Anne is rough.[(triple4)] Anne is white.[(triple5 OR ((triple1) -> rule2) OR ((triple4) -> rule1) OR ((((triple3) -> rule3)) -> rule2))] Fiona is cold.[(triple6)] Fiona is nice.[(triple8)] Fiona is not kind.[(triple7)] Fiona is white.[(triple9 OR ((((triple8) -> rule3)) -> rule2))] Fiona is young.[(triple10)] @1: Fiona is big.[(((triple8) -> rule3))] @2: Fiona is not rough.[(((((triple8) -> rule3) triple10) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple3) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((triple1 triple4) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple3) -> (rule3 % int2)) triple4) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
triple5
((triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple4) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
Fiona is nice.
("Fiona" "is" "nice" "+")
triple8
Fiona is not kind.
("Fiona" "is" "kind" "-")
triple7
Fiona is white.
("Fiona" "is" "white" "+")
triple9
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
triple10
Fiona is big.
("Fiona" "is" "big" "+")
((triple8) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not rough.
("Fiona" "is" "rough" "-")
((((triple8) -> (rule3 % int2)) triple10) -> (rule5 % int1))
Fiona is not rough.
("Fiona" "is" "rough" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2