Charlie is young. Fiona is big. Harry is big. If Charlie is smart then Charlie is big. If Fiona is young then Fiona is rough. If something is young then it is smart. If Harry is smart then Harry is not young. Big things are not round. If Fiona is not rough then Fiona is smart.
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Harry is big.
("Harry" "is" "big" "+")
If Charlie is smart then Charlie is big.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "big" "+"))
If Fiona is young then Fiona is rough.
((("Fiona" "is" "young" "+")) -> ("Fiona" "is" "rough" "+"))
If something is young then it is smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If Harry is smart then Harry is not young.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "young" "-"))
Big things are not round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "-"))
If Fiona is not rough then Fiona is smart.
((("Fiona" "is" "rough" "~")) -> ("Fiona" "is" "smart" "+"))
Charlie is young.
True
1
proof
[(triple1)]
("Charlie" "is" "young" "+")
triple1
Fiona is not big.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "big" "-")
triple2
Fiona is not round.
True
2
proof
[(((triple2) -> rule5))]
("Fiona" "is" "round" "-")
((triple2) -> (rule5 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
Harry is round.
False
2
inv-proof
[(((triple3) -> rule5))]
("Harry" "is" "round" "+")
((triple3) -> (rule5 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Charlie is big.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Charlie" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not big.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Charlie" "is" "big" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not round.
True
4
proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule5))]
("Charlie" "is" "round" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is round.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule5))]
("Charlie" "is" "round" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "rough" "-")
Harry is smart.
Unknown
rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "smart" "+")
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "smart" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Charlie is young.[(triple1)] Fiona is big.[(triple2)] Harry is big.[(triple3)] @1: Charlie is smart.[(((triple1) -> rule3))] Fiona is not round.[(((triple2) -> rule5))] Harry is not round.[(((triple3) -> rule5))] @2: Charlie is big.[(((((triple1) -> rule3)) -> rule1))] @3: Charlie is not round.[(((((((triple1) -> rule3)) -> rule1)) -> rule5))]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Fiona is big.
("Fiona" "is" "big" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Fiona is not round.
("Fiona" "is" "round" "-")
((triple2) -> (rule5 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
Harry is not round.
("Harry" "is" "round" "-")
((triple3) -> (rule5 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not round.
("Charlie" "is" "round" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3