Charlie is blue. Charlie is cold. Charlie is furry. Charlie is round. Erin is big. Erin is quiet. Erin is young. Fiona is blue. Fiona is round. Fiona is not young. All round, big things are not young. All quiet things are young. If something is furry and not quiet then it is not young. Cold things are big. If something is cold and blue then it is big. If something is cold then it is furry. Young, big things are not furry. If Charlie is cold and Charlie is young then Charlie is round.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is not young.
("Fiona" "is" "young" "-")
All round, big things are not young.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "-"))
All quiet things are young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
If something is furry and not quiet then it is not young.
((("something" "is" "furry" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "young" "-"))
Cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If something is cold and blue then it is big.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is cold then it is furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
Young, big things are not furry.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "-"))
If Charlie is cold and Charlie is young then Charlie is round.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "round" "+"))
Erin is quiet.
True
1
proof
[(triple6)]
("Erin" "is" "quiet" "+")
triple6
Erin is not young.
False
1
inv-proof
[(triple7 OR ((triple6) -> rule2))]
("Erin" "is" "young" "-")
triple7
((triple6) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not furry.
True
3
proof
[(((triple7 triple5) -> rule7) OR ((((triple6) -> rule2) triple5) -> rule7))]
("Erin" "is" "furry" "-")
((triple7 triple5) -> (rule7 % int1))
Erin is not furry.
("Erin" "is" "furry" "-")
int1
((((triple6) -> (rule2 % int2)) triple5) -> (rule7 % int1))
Erin is not furry.
("Erin" "is" "furry" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is furry.
False
3
inv-proof
[(((triple7 triple5) -> rule7) OR ((((triple6) -> rule2) triple5) -> rule7))]
("Erin" "is" "furry" "+")
((triple7 triple5) -> (rule7 % int1))
Erin is not furry.
("Erin" "is" "furry" "-")
int1
((((triple6) -> (rule2 % int2)) triple5) -> (rule7 % int1))
Erin is not furry.
("Erin" "is" "furry" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Charlie is not young.
True
4
proof
[(((triple4 ((triple2) -> rule4)) -> rule1) OR ((triple4 ((triple2 triple1) -> rule5)) -> rule1))]
("Charlie" "is" "young" "-")
((triple4 ((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple4 ((triple2 triple1) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
False
4
inv-proof
[(((triple4 ((triple2) -> rule4)) -> rule1) OR ((triple4 ((triple2 triple1) -> rule5)) -> rule1))]
("Charlie" "is" "young" "+")
((triple4 ((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple4 ((triple2 triple1) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "big" "-")
Fiona is furry.
Unknown
rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "furry" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2)] Charlie is furry.[(triple3 OR ((triple2) -> rule6))] Charlie is round.[(triple4)] Erin is big.[(triple5)] Erin is quiet.[(triple6)] Erin is young.[(triple7 OR ((triple6) -> rule2))] Fiona is blue.[(triple8)] Fiona is not young.[(triple10)] Fiona is round.[(triple9)] @1: Charlie is big.[(((triple2) -> rule4) OR ((triple2 triple1) -> rule5))] Erin is not furry.[(((triple7 triple5) -> rule7) OR ((((triple6) -> rule2) triple5) -> rule7))] @2: Charlie is not young.[(((triple4 ((triple2) -> rule4)) -> rule1) OR ((triple4 ((triple2 triple1) -> rule5)) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
((triple2) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
((triple6) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple8
Fiona is not young.
("Fiona" "is" "young" "-")
triple10
Fiona is round.
("Fiona" "is" "round" "+")
triple9
Charlie is big.
("Charlie" "is" "big" "+")
((triple2) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple2 triple1) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Erin is not furry.
("Erin" "is" "furry" "-")
((triple7 triple5) -> (rule7 % int1))
Erin is not furry.
("Erin" "is" "furry" "-")
int1
((((triple6) -> (rule2 % int2)) triple5) -> (rule7 % int1))
Erin is not furry.
("Erin" "is" "furry" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Charlie is not young.
("Charlie" "is" "young" "-")
((triple4 ((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple4 ((triple2 triple1) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2