Anne is rough. Anne is round. Bob is kind. Bob is round. Charlie is big. Charlie is young. Erin is smart. If something is cold and kind then it is big. Rough things are smart. If Bob is round then Bob is big. If something is smart then it is big. All big things are rough. Big, smart things are young.
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If something is cold and kind then it is big.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
Rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If Bob is round then Bob is big.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "big" "+"))
If something is smart then it is big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
All big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Big, smart things are young.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Bob is kind.
True
1
proof
[(triple3)]
("Bob" "is" "kind" "+")
triple3
Charlie is not big.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "big" "-")
triple5
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Anne is rough.[(triple1)] Anne is round.[(triple2)] Bob is kind.[(triple3)] Bob is round.[(triple4)] Charlie is big.[(triple5)] Charlie is young.[(triple6 OR ((triple5 ((((triple5) -> rule5)) -> rule2)) -> rule6))] Erin is smart.[(triple7)] @1: Anne is smart.[(((triple1) -> rule2))] Bob is big.[(((triple4) -> rule3))] Charlie is rough.[(((triple5) -> rule5))] Erin is big.[(((triple7) -> rule4))] @2: Anne is big.[(((((triple1) -> rule2)) -> rule4))] Bob is rough.[(((((triple4) -> rule3)) -> rule5))] Charlie is smart.[(((((triple5) -> rule5)) -> rule2))] Erin is rough.[(((((triple7) -> rule4)) -> rule5))] Erin is young.[(((((triple7) -> rule4) triple7) -> rule6))] @3: Anne is young.[(((((((triple1) -> rule2)) -> rule4) ((triple1) -> rule2)) -> rule6))] Bob is smart.[(((((((triple4) -> rule3)) -> rule5)) -> rule2))] @4: Bob is young.[(((((triple4) -> rule3) ((((((triple4) -> rule3)) -> rule5)) -> rule2)) -> rule6))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
((triple5 ((((triple5) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((triple4) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple5) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple7) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple7) -> (rule4 % int2))) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((((triple7) -> (rule4 % int2)) triple7) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2)) ((triple1) -> (rule2 % int3))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
((((triple4) -> (rule3 % int4)) ((((((triple4) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4